Metamath Proof Explorer

Theorem corcltrcl

Description: The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 17-Jun-2020)

Ref Expression
Assertion corcltrcl ( r* ∘ t+ ) = t*

Proof

Step Hyp Ref Expression
1 dfrcl4 ⊢ r* = ( 𝑎 ∈ V ↦ ∪ 𝑖 ∈ { 0 , 1 } ( 𝑎 ↑𝑟 𝑖 ) )
2 dftrcl3 ⊢ t+ = ( 𝑏 ∈ V ↦ ∪ 𝑗 ∈ ℕ ( 𝑏 ↑𝑟 𝑗 ) )
3 dfrtrcl3 ⊢ t* = ( 𝑐 ∈ V ↦ ∪ 𝑘 ∈ ℕ0 ( 𝑐 ↑𝑟 𝑘 ) )
4 prex ⊢ { 0 , 1 } ∈ V
5 nnex ⊢ ℕ ∈ V
6 df-n0 ⊢ ℕ0 = ( ℕ ∪ { 0 } )
7 uncom ⊢ ( ℕ ∪ { 0 } ) = ( { 0 } ∪ ℕ )
8 df-pr ⊢ { 0 , 1 } = ( { 0 } ∪ { 1 } )
9 8 uneq1i ⊢ ( { 0 , 1 } ∪ ℕ ) = ( ( { 0 } ∪ { 1 } ) ∪ ℕ )
10 unass ⊢ ( ( { 0 } ∪ { 1 } ) ∪ ℕ ) = ( { 0 } ∪ ( { 1 } ∪ ℕ ) )
11 1nn ⊢ 1 ∈ ℕ
12 snssi ⊢ ( 1 ∈ ℕ → { 1 } ⊆ ℕ )
13 11 12 ax-mp ⊢ { 1 } ⊆ ℕ
14 ssequn1 ⊢ ( { 1 } ⊆ ℕ ↔ ( { 1 } ∪ ℕ ) = ℕ )
15 13 14 mpbi ⊢ ( { 1 } ∪ ℕ ) = ℕ
16 15 uneq2i ⊢ ( { 0 } ∪ ( { 1 } ∪ ℕ ) ) = ( { 0 } ∪ ℕ )
17 9 10 16 3eqtrri ⊢ ( { 0 } ∪ ℕ ) = ( { 0 , 1 } ∪ ℕ )
18 6 7 17 3eqtri ⊢ ℕ0 = ( { 0 , 1 } ∪ ℕ )
19 oveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑑 ↑𝑟 𝑘 ) = ( 𝑑 ↑𝑟 𝑖 ) )
20 19 cbviunv ⊢ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) = ∪ 𝑖 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑖 )
21 ss2iun ⊢ ( ∀ 𝑖 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑖 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) → ∪ 𝑖 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑖 ) ⊆ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
22 relexp1g ⊢ ( 𝑑 ∈ V → ( 𝑑 ↑𝑟 1 ) = 𝑑 )
23 22 elv ⊢ ( 𝑑 ↑𝑟 1 ) = 𝑑
24 oveq2 ⊢ ( 𝑗 = 1 → ( 𝑑 ↑𝑟 𝑗 ) = ( 𝑑 ↑𝑟 1 ) )
25 24 ssiun2s ⊢ ( 1 ∈ ℕ → ( 𝑑 ↑𝑟 1 ) ⊆ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) )
26 11 25 ax-mp ⊢ ( 𝑑 ↑𝑟 1 ) ⊆ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 )
27 23 26 eqsstrri ⊢ 𝑑 ⊆ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 )
28 27 a1i ⊢ ( 𝑖 ∈ { 0 , 1 } → 𝑑 ⊆ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) )
29 ovex ⊢ ( 𝑑 ↑𝑟 𝑗 ) ∈ V
30 5 29 iunex ⊢ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ∈ V
31 30 a1i ⊢ ( 𝑖 ∈ { 0 , 1 } → ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ∈ V )
32 0nn0 ⊢ 0 ∈ ℕ0
33 1nn0 ⊢ 1 ∈ ℕ0
34 prssi ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → { 0 , 1 } ⊆ ℕ0 )
35 32 33 34 mp2an ⊢ { 0 , 1 } ⊆ ℕ0
36 35 sseli ⊢ ( 𝑖 ∈ { 0 , 1 } → 𝑖 ∈ ℕ0 )
37 28 31 36 relexpss1d ⊢ ( 𝑖 ∈ { 0 , 1 } → ( 𝑑 ↑𝑟 𝑖 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
38 21 37 mprg ⊢ ∪ 𝑖 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑖 ) ⊆ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
39 20 38 eqsstri ⊢ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ⊆ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
40 oveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑑 ↑𝑟 𝑘 ) = ( 𝑑 ↑𝑟 𝑗 ) )
41 40 cbviunv ⊢ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) = ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 )
42 relexp1g ⊢ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ∈ V → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) )
43 30 42 ax-mp ⊢ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 )
44 41 43 eqtr4i ⊢ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) = ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 )
45 1ex ⊢ 1 ∈ V
46 45 prid2 ⊢ 1 ∈ { 0 , 1 }
47 oveq2 ⊢ ( 𝑖 = 1 → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) )
48 47 ssiun2s ⊢ ( 1 ∈ { 0 , 1 } → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) ⊆ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
49 46 48 ax-mp ⊢ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) ⊆ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
50 44 49 eqsstri ⊢ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ⊆ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
51 c0ex ⊢ 0 ∈ V
52 51 prid1 ⊢ 0 ∈ { 0 , 1 }
53 oveq2 ⊢ ( 𝑘 = 0 → ( 𝑑 ↑𝑟 𝑘 ) = ( 𝑑 ↑𝑟 0 ) )
54 53 ssiun2s ⊢ ( 0 ∈ { 0 , 1 } → ( 𝑑 ↑𝑟 0 ) ⊆ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) )
55 52 54 ax-mp ⊢ ( 𝑑 ↑𝑟 0 ) ⊆ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 )
56 ssid ⊢ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 )
57 unss12 ⊢ ( ( ( 𝑑 ↑𝑟 0 ) ⊆ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ∧ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) → ( ( 𝑑 ↑𝑟 0 ) ∪ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) ⊆ ( ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ∪ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) )
58 55 56 57 mp2an ⊢ ( ( 𝑑 ↑𝑟 0 ) ∪ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) ⊆ ( ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ∪ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) )
59 iuneq1 ⊢ ( { 0 , 1 } = ( { 0 } ∪ { 1 } ) → ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ∪ 𝑖 ∈ ( { 0 } ∪ { 1 } ) ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
60 8 59 ax-mp ⊢ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ∪ 𝑖 ∈ ( { 0 } ∪ { 1 } ) ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
61 iunxun ⊢ ∪ 𝑖 ∈ ( { 0 } ∪ { 1 } ) ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑖 ∈ { 0 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ∪ ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
62 oveq2 ⊢ ( 𝑖 = 0 → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 0 ) )
63 51 62 iunxsn ⊢ ∪ 𝑖 ∈ { 0 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 0 )
64 vex ⊢ 𝑑 ∈ V
65 nnssnn0 ⊢ ℕ ⊆ ℕ0
66 inelcm ⊢ ( ( 1 ∈ { 0 , 1 } ∧ 1 ∈ ℕ ) → ( { 0 , 1 } ∩ ℕ ) ≠ ∅ )
67 46 11 66 mp2an ⊢ ( { 0 , 1 } ∩ ℕ ) ≠ ∅
68 iunrelexp0 ⊢ ( ( 𝑑 ∈ V ∧ ℕ ⊆ ℕ0 ∧ ( { 0 , 1 } ∩ ℕ ) ≠ ∅ ) → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 0 ) = ( 𝑑 ↑𝑟 0 ) )
69 64 65 67 68 mp3an ⊢ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 0 ) = ( 𝑑 ↑𝑟 0 )
70 63 69 eqtri ⊢ ∪ 𝑖 ∈ { 0 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( 𝑑 ↑𝑟 0 )
71 45 47 iunxsn ⊢ ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 )
72 43 41 eqtr4i ⊢ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 )
73 71 72 eqtri ⊢ ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 )
74 70 73 uneq12i ⊢ ( ∪ 𝑖 ∈ { 0 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ∪ ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ) = ( ( 𝑑 ↑𝑟 0 ) ∪ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) )
75 60 61 74 3eqtri ⊢ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ( 𝑑 ↑𝑟 0 ) ∪ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) )
76 iunxun ⊢ ∪ 𝑘 ∈ ( { 0 , 1 } ∪ ℕ ) ( 𝑑 ↑𝑟 𝑘 ) = ( ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ∪ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) )
77 58 75 76 3sstr4i ⊢ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ( { 0 , 1 } ∪ ℕ ) ( 𝑑 ↑𝑟 𝑘 )
78 1 2 3 4 5 18 39 50 77 comptiunov2i ⊢ ( r* ∘ t+ ) = t*