Metamath Proof Explorer

Theorem relexprelg

Description: The exponentiation of a class is a relation except when the exponent is one and the class is not a relation. (Contributed by RP, 23-May-2020)

Ref Expression
Assertion relexprelg ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ ( 𝑁 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 eqeq1 ⊢ ( 𝑛 = 1 → ( 𝑛 = 1 ↔ 1 = 1 ) )
3 2 imbi1d ⊢ ( 𝑛 = 1 → ( ( 𝑛 = 1 → Rel 𝑅 ) ↔ ( 1 = 1 → Rel 𝑅 ) ) )
4 3 anbi2d ⊢ ( 𝑛 = 1 → ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑛 = 1 → Rel 𝑅 ) ) ↔ ( 𝑅 ∈ 𝑉 ∧ ( 1 = 1 → Rel 𝑅 ) ) ) )
5 oveq2 ⊢ ( 𝑛 = 1 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 1 ) )
6 5 releqd ⊢ ( 𝑛 = 1 → ( Rel ( 𝑅 ↑𝑟 𝑛 ) ↔ Rel ( 𝑅 ↑𝑟 1 ) ) )
7 4 6 imbi12d ⊢ ( 𝑛 = 1 → ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑛 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑛 ) ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( 1 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 1 ) ) ) )
8 eqeq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 = 1 ↔ 𝑚 = 1 ) )
9 8 imbi1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑛 = 1 → Rel 𝑅 ) ↔ ( 𝑚 = 1 → Rel 𝑅 ) ) )
10 9 anbi2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑛 = 1 → Rel 𝑅 ) ) ↔ ( 𝑅 ∈ 𝑉 ∧ ( 𝑚 = 1 → Rel 𝑅 ) ) ) )
11 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑚 ) )
12 11 releqd ⊢ ( 𝑛 = 𝑚 → ( Rel ( 𝑅 ↑𝑟 𝑛 ) ↔ Rel ( 𝑅 ↑𝑟 𝑚 ) ) )
13 10 12 imbi12d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑛 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑛 ) ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑚 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑚 ) ) ) )
14 eqeq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 = 1 ↔ ( 𝑚 + 1 ) = 1 ) )
15 14 imbi1d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑛 = 1 → Rel 𝑅 ) ↔ ( ( 𝑚 + 1 ) = 1 → Rel 𝑅 ) ) )
16 15 anbi2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑛 = 1 → Rel 𝑅 ) ) ↔ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑚 + 1 ) = 1 → Rel 𝑅 ) ) ) )
17 oveq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
18 17 releqd ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( Rel ( 𝑅 ↑𝑟 𝑛 ) ↔ Rel ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) )
19 16 18 imbi12d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑛 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑛 ) ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑚 + 1 ) = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) ) )
20 eqeq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 = 1 ↔ 𝑁 = 1 ) )
21 20 imbi1d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 = 1 → Rel 𝑅 ) ↔ ( 𝑁 = 1 → Rel 𝑅 ) ) )
22 21 anbi2d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑛 = 1 → Rel 𝑅 ) ) ↔ ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = 1 → Rel 𝑅 ) ) ) )
23 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑁 ) )
24 23 releqd ⊢ ( 𝑛 = 𝑁 → ( Rel ( 𝑅 ↑𝑟 𝑛 ) ↔ Rel ( 𝑅 ↑𝑟 𝑁 ) ) )
25 22 24 imbi12d ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑛 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑛 ) ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑁 ) ) ) )
26 eqid ⊢ 1 = 1
27 pm2.27 ⊢ ( 1 = 1 → ( ( 1 = 1 → Rel 𝑅 ) → Rel 𝑅 ) )
28 26 27 ax-mp ⊢ ( ( 1 = 1 → Rel 𝑅 ) → Rel 𝑅 )
29 28 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 1 = 1 → Rel 𝑅 ) ) → Rel 𝑅 )
30 relexp1g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
31 30 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 1 = 1 → Rel 𝑅 ) ) → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
32 31 releqd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 1 = 1 → Rel 𝑅 ) ) → ( Rel ( 𝑅 ↑𝑟 1 ) ↔ Rel 𝑅 ) )
33 29 32 mpbird ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 1 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 1 ) )
34 relco ⊢ Rel ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 )
35 relexpsucnnr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
36 35 ancoms ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
37 36 releqd ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( Rel ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ↔ Rel ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) ) )
38 34 37 mpbiri ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
39 38 a1d ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( ( ( 𝑚 + 1 ) = 1 → Rel 𝑅 ) → Rel ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) )
40 39 expimpd ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑚 + 1 ) = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) )
41 40 a1d ⊢ ( 𝑚 ∈ ℕ → ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑚 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑚 ) ) → ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑚 + 1 ) = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) ) )
42 7 13 19 25 33 41 nnind ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑁 ) ) )
43 relexp0rel ⊢ ( 𝑅 ∈ 𝑉 → Rel ( 𝑅 ↑𝑟 0 ) )
44 43 adantl ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 0 ) )
45 simpl ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 = 0 )
46 45 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( 𝑅 ↑𝑟 0 ) )
47 46 releqd ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( Rel ( 𝑅 ↑𝑟 𝑁 ) ↔ Rel ( 𝑅 ↑𝑟 0 ) ) )
48 44 47 mpbird ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )
49 48 a1d ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑁 = 1 → Rel 𝑅 ) → Rel ( 𝑅 ↑𝑟 𝑁 ) ) )
50 49 expimpd ⊢ ( 𝑁 = 0 → ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑁 ) ) )
51 42 50 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑁 ) ) )
52 1 51 sylbi ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑁 ) ) )
53 52 3impib ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ ( 𝑁 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )