Theorem relexpuzrel

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

	Ref	Expression
Assertion	relexpuzrel	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eluzge2nn0	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ0 )
2	1	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ ℕ0 )
3		simpr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 )
4		eluz2b3	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) )
5	4	simprbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≠ 1 )
6	5	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ≠ 1 )
7	6	neneqd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ¬ 𝑁 = 1 )
8	7	pm2.21d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 = 1 → Rel 𝑅 ) )
9		relexprelg	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ ( 𝑁 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )
10	2 3 8 9	syl3anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )