Metamath Proof Explorer

Theorem relexpcnv

Description: Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020)

Ref Expression
Assertion relexpcnv ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 oveq2 ⊢ ( 𝑛 = 1 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 1 ) )
3 2 cnveqd ⊢ ( 𝑛 = 1 → ◡ ( 𝑅 ↑𝑟 𝑛 ) = ◡ ( 𝑅 ↑𝑟 1 ) )
4 oveq2 ⊢ ( 𝑛 = 1 → ( ◡ 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 1 ) )
5 3 4 eqeq12d ⊢ ( 𝑛 = 1 → ( ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) ↔ ◡ ( 𝑅 ↑𝑟 1 ) = ( ◡ 𝑅 ↑𝑟 1 ) ) )
6 5 imbi2d ⊢ ( 𝑛 = 1 → ( ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) ) ↔ ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 1 ) = ( ◡ 𝑅 ↑𝑟 1 ) ) ) )
7 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑚 ) )
8 7 cnveqd ⊢ ( 𝑛 = 𝑚 → ◡ ( 𝑅 ↑𝑟 𝑛 ) = ◡ ( 𝑅 ↑𝑟 𝑚 ) )
9 oveq2 ⊢ ( 𝑛 = 𝑚 → ( ◡ 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) )
10 8 9 eqeq12d ⊢ ( 𝑛 = 𝑚 → ( ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) ↔ ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) )
11 10 imbi2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) ) ↔ ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) ) )
12 oveq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
13 12 cnveqd ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ◡ ( 𝑅 ↑𝑟 𝑛 ) = ◡ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
14 oveq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ◡ 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
15 13 14 eqeq12d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) ↔ ◡ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ◡ 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) )
16 15 imbi2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) ) ↔ ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ◡ 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) ) )
17 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑁 ) )
18 17 cnveqd ⊢ ( 𝑛 = 𝑁 → ◡ ( 𝑅 ↑𝑟 𝑛 ) = ◡ ( 𝑅 ↑𝑟 𝑁 ) )
19 oveq2 ⊢ ( 𝑛 = 𝑁 → ( ◡ 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) )
20 18 19 eqeq12d ⊢ ( 𝑛 = 𝑁 → ( ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) ↔ ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) ) )
21 20 imbi2d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) ) ↔ ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) ) ) )
22 relexp1g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
23 22 cnveqd ⊢ ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 1 ) = ◡ 𝑅 )
24 cnvexg ⊢ ( 𝑅 ∈ 𝑉 → ◡ 𝑅 ∈ V )
25 relexp1g ⊢ ( ◡ 𝑅 ∈ V → ( ◡ 𝑅 ↑𝑟 1 ) = ◡ 𝑅 )
26 24 25 syl ⊢ ( 𝑅 ∈ 𝑉 → ( ◡ 𝑅 ↑𝑟 1 ) = ◡ 𝑅 )
27 23 26 eqtr4d ⊢ ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 1 ) = ( ◡ 𝑅 ↑𝑟 1 ) )
28 cnvco ⊢ ◡ ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) = ( ◡ 𝑅 ∘ ◡ ( 𝑅 ↑𝑟 𝑚 ) )
29 simp3 ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) → ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) )
30 29 coeq2d ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) → ( ◡ 𝑅 ∘ ◡ ( 𝑅 ↑𝑟 𝑚 ) ) = ( ◡ 𝑅 ∘ ( ◡ 𝑅 ↑𝑟 𝑚 ) ) )
31 28 30 eqtrid ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) → ◡ ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) = ( ◡ 𝑅 ∘ ( ◡ 𝑅 ↑𝑟 𝑚 ) ) )
32 simp2 ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) → 𝑅 ∈ 𝑉 )
33 simp1 ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) → 𝑚 ∈ ℕ )
34 relexpsucnnr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
35 32 33 34 syl2anc ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
36 35 cnveqd ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) → ◡ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ◡ ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
37 32 24 syl ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) → ◡ 𝑅 ∈ V )
38 relexpsucnnl ⊢ ( ( ◡ 𝑅 ∈ V ∧ 𝑚 ∈ ℕ ) → ( ◡ 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ◡ 𝑅 ∘ ( ◡ 𝑅 ↑𝑟 𝑚 ) ) )
39 37 33 38 syl2anc ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) → ( ◡ 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ◡ 𝑅 ∘ ( ◡ 𝑅 ↑𝑟 𝑚 ) ) )
40 31 36 39 3eqtr4d ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) → ◡ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ◡ 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
41 40 3exp ⊢ ( 𝑚 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) → ◡ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ◡ 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) ) )
42 41 a2d ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 𝑚 ) = ( ◡ 𝑅 ↑𝑟 𝑚 ) ) → ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ◡ 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ) ) )
43 6 11 16 21 27 42 nnind ⊢ ( 𝑁 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) ) )
44 cnvresid ⊢ ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
45 uncom ⊢ ( dom 𝑅 ∪ ran 𝑅 ) = ( ran 𝑅 ∪ dom 𝑅 )
46 df-rn ⊢ ran 𝑅 = dom ◡ 𝑅
47 dfdm4 ⊢ dom 𝑅 = ran ◡ 𝑅
48 46 47 uneq12i ⊢ ( ran 𝑅 ∪ dom 𝑅 ) = ( dom ◡ 𝑅 ∪ ran ◡ 𝑅 )
49 45 48 eqtri ⊢ ( dom 𝑅 ∪ ran 𝑅 ) = ( dom ◡ 𝑅 ∪ ran ◡ 𝑅 )
50 49 reseq2i ⊢ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( I ↾ ( dom ◡ 𝑅 ∪ ran ◡ 𝑅 ) )
51 44 50 eqtri ⊢ ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( I ↾ ( dom ◡ 𝑅 ∪ ran ◡ 𝑅 ) )
52 oveq2 ⊢ ( 𝑁 = 0 → ( 𝑅 ↑𝑟 𝑁 ) = ( 𝑅 ↑𝑟 0 ) )
53 relexp0g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
54 52 53 sylan9eq ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
55 54 cnveqd ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
56 oveq2 ⊢ ( 𝑁 = 0 → ( ◡ 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 0 ) )
57 56 adantr ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ◡ 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 0 ) )
58 simpr ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 )
59 relexp0g ⊢ ( ◡ 𝑅 ∈ V → ( ◡ 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom ◡ 𝑅 ∪ ran ◡ 𝑅 ) ) )
60 58 24 59 3syl ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ◡ 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom ◡ 𝑅 ∪ ran ◡ 𝑅 ) ) )
61 57 60 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ◡ 𝑅 ↑𝑟 𝑁 ) = ( I ↾ ( dom ◡ 𝑅 ∪ ran ◡ 𝑅 ) ) )
62 51 55 61 3eqtr4a ⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) )
63 62 ex ⊢ ( 𝑁 = 0 → ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) ) )
64 43 63 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) ) )
65 1 64 sylbi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑅 ∈ 𝑉 → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) ) )
66 65 imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) )