Theorem relexpuzrel

Description: The exponentiation of a class to an integer not smaller than 2 is a relation. (Contributed by RP, 23-May-2020)

	Ref	Expression
Assertion	relexpuzrel	|- ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r N ) )

Proof

Step	Hyp	Ref	Expression
1		eluzge2nn0	|- ( N e. ( ZZ>= ` 2 ) -> N e. NN0 )
2	1	adantr	|- ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> N e. NN0 )
3		simpr	|- ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> R e. V )
4		eluz2b3	|- ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ N =/= 1 ) )
5	4	simprbi	|- ( N e. ( ZZ>= ` 2 ) -> N =/= 1 )
6	5	adantr	|- ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> N =/= 1 )
7	6	neneqd	|- ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> -. N = 1 )
8	7	pm2.21d	|- ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N = 1 -> Rel R ) )
9		relexprelg	|- ( ( N e. NN0 /\ R e. V /\ ( N = 1 -> Rel R ) ) -> Rel ( R ^r N ) )
10	2 3 8 9	syl3anc	|- ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r N ) )