Metamath Proof Explorer


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 ( ( 𝑁 ∈ ( ℤ ‘ 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 ( 𝑅𝑟 𝑁 ) )