Metamath Proof Explorer

Theorem cotrclrcl

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

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

Proof

Step Hyp Ref Expression
1 dftrcl3 ⊢ t+ = ( 𝑎 ∈ V ↦ ∪ 𝑖 ∈ ℕ ( 𝑎 ↑𝑟 𝑖 ) )
2 dfrcl4 ⊢ r* = ( 𝑏 ∈ V ↦ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑏 ↑𝑟 𝑗 ) )
3 dfrtrcl3 ⊢ t* = ( 𝑐 ∈ V ↦ ∪ 𝑘 ∈ ℕ0 ( 𝑐 ↑𝑟 𝑘 ) )
4 nnex ⊢ ℕ ∈ V
5 prex ⊢ { 0 , 1 } ∈ V
6 df-n0 ⊢ ℕ0 = ( ℕ ∪ { 0 } )
7 df-pr ⊢ { 0 , 1 } = ( { 0 } ∪ { 1 } )
8 7 equncomi ⊢ { 0 , 1 } = ( { 1 } ∪ { 0 } )
9 8 uneq2i ⊢ ( ℕ ∪ { 0 , 1 } ) = ( ℕ ∪ ( { 1 } ∪ { 0 } ) )
10 unass ⊢ ( ( ℕ ∪ { 1 } ) ∪ { 0 } ) = ( ℕ ∪ ( { 1 } ∪ { 0 } ) )
11 1nn ⊢ 1 ∈ ℕ
12 snssi ⊢ ( 1 ∈ ℕ → { 1 } ⊆ ℕ )
13 11 12 ax-mp ⊢ { 1 } ⊆ ℕ
14 ssequn2 ⊢ ( { 1 } ⊆ ℕ ↔ ( ℕ ∪ { 1 } ) = ℕ )
15 13 14 mpbi ⊢ ( ℕ ∪ { 1 } ) = ℕ
16 15 uneq1i ⊢ ( ( ℕ ∪ { 1 } ) ∪ { 0 } ) = ( ℕ ∪ { 0 } )
17 9 10 16 3eqtr2ri ⊢ ( ℕ ∪ { 0 } ) = ( ℕ ∪ { 0 , 1 } )
18 6 17 eqtri ⊢ ℕ0 = ( ℕ ∪ { 0 , 1 } )
19 oveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑑 ↑𝑟 𝑘 ) = ( 𝑑 ↑𝑟 𝑖 ) )
20 19 cbviunv ⊢ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) = ∪ 𝑖 ∈ ℕ ( 𝑑 ↑𝑟 𝑖 )
21 ss2iun ⊢ ( ∀ 𝑖 ∈ ℕ ( 𝑑 ↑𝑟 𝑖 ) ⊆ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) → ∪ 𝑖 ∈ ℕ ( 𝑑 ↑𝑟 𝑖 ) ⊆ ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
22 1ex ⊢ 1 ∈ V
23 22 prid2 ⊢ 1 ∈ { 0 , 1 }
24 oveq2 ⊢ ( 𝑗 = 1 → ( 𝑑 ↑𝑟 𝑗 ) = ( 𝑑 ↑𝑟 1 ) )
25 relexp1g ⊢ ( 𝑑 ∈ V → ( 𝑑 ↑𝑟 1 ) = 𝑑 )
26 25 elv ⊢ ( 𝑑 ↑𝑟 1 ) = 𝑑
27 24 26 eqtrdi ⊢ ( 𝑗 = 1 → ( 𝑑 ↑𝑟 𝑗 ) = 𝑑 )
28 27 ssiun2s ⊢ ( 1 ∈ { 0 , 1 } → 𝑑 ⊆ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) )
29 23 28 ax-mp ⊢ 𝑑 ⊆ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 )
30 29 a1i ⊢ ( 𝑖 ∈ ℕ → 𝑑 ⊆ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) )
31 ovex ⊢ ( 𝑑 ↑𝑟 𝑗 ) ∈ V
32 5 31 iunex ⊢ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ∈ V
33 32 a1i ⊢ ( 𝑖 ∈ ℕ → ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ∈ V )
34 nnnn0 ⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℕ0 )
35 30 33 34 relexpss1d ⊢ ( 𝑖 ∈ ℕ → ( 𝑑 ↑𝑟 𝑖 ) ⊆ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
36 21 35 mprg ⊢ ∪ 𝑖 ∈ ℕ ( 𝑑 ↑𝑟 𝑖 ) ⊆ ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
37 20 36 eqsstri ⊢ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ⊆ ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
38 oveq2 ⊢ ( 𝑖 = 1 → ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) )
39 relexp1g ⊢ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ∈ V → ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) )
40 32 39 ax-mp ⊢ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 )
41 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑑 ↑𝑟 𝑗 ) = ( 𝑑 ↑𝑟 𝑘 ) )
42 41 cbviunv ⊢ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) = ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 )
43 40 42 eqtri ⊢ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 )
44 38 43 eqtrdi ⊢ ( 𝑖 = 1 → ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) )
45 44 ssiun2s ⊢ ( 1 ∈ ℕ → ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ⊆ ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
46 11 45 ax-mp ⊢ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ⊆ ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
47 iunss ⊢ ( ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ↔ ∀ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) )
48 iuneq1 ⊢ ( { 0 , 1 } = ( { 0 } ∪ { 1 } ) → ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) = ∪ 𝑗 ∈ ( { 0 } ∪ { 1 } ) ( 𝑑 ↑𝑟 𝑗 ) )
49 7 48 ax-mp ⊢ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) = ∪ 𝑗 ∈ ( { 0 } ∪ { 1 } ) ( 𝑑 ↑𝑟 𝑗 )
50 iunxun ⊢ ∪ 𝑗 ∈ ( { 0 } ∪ { 1 } ) ( 𝑑 ↑𝑟 𝑗 ) = ( ∪ 𝑗 ∈ { 0 } ( 𝑑 ↑𝑟 𝑗 ) ∪ ∪ 𝑗 ∈ { 1 } ( 𝑑 ↑𝑟 𝑗 ) )
51 c0ex ⊢ 0 ∈ V
52 oveq2 ⊢ ( 𝑗 = 0 → ( 𝑑 ↑𝑟 𝑗 ) = ( 𝑑 ↑𝑟 0 ) )
53 51 52 iunxsn ⊢ ∪ 𝑗 ∈ { 0 } ( 𝑑 ↑𝑟 𝑗 ) = ( 𝑑 ↑𝑟 0 )
54 22 24 iunxsn ⊢ ∪ 𝑗 ∈ { 1 } ( 𝑑 ↑𝑟 𝑗 ) = ( 𝑑 ↑𝑟 1 )
55 53 54 uneq12i ⊢ ( ∪ 𝑗 ∈ { 0 } ( 𝑑 ↑𝑟 𝑗 ) ∪ ∪ 𝑗 ∈ { 1 } ( 𝑑 ↑𝑟 𝑗 ) ) = ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) )
56 49 50 55 3eqtri ⊢ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) = ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) )
57 56 oveq1i ⊢ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑖 )
58 oveq2 ⊢ ( 𝑥 = 1 → ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑥 ) = ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 1 ) )
59 58 sseq1d ⊢ ( 𝑥 = 1 → ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑥 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ↔ ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 1 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ) )
60 oveq2 ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑥 ) = ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) )
61 60 sseq1d ⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑥 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ↔ ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ) )
62 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑥 ) = ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 ( 𝑦 + 1 ) ) )
63 62 sseq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑥 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ↔ ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ) )
64 oveq2 ⊢ ( 𝑥 = 𝑖 → ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑥 ) = ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑖 ) )
65 64 sseq1d ⊢ ( 𝑥 = 𝑖 → ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑥 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ↔ ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ) )
66 ovex ⊢ ( 𝑑 ↑𝑟 0 ) ∈ V
67 ovex ⊢ ( 𝑑 ↑𝑟 1 ) ∈ V
68 66 67 unex ⊢ ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ∈ V
69 relexp1g ⊢ ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ∈ V → ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 1 ) = ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) )
70 68 69 ax-mp ⊢ ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 1 ) = ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) )
71 0nn0 ⊢ 0 ∈ ℕ0
72 oveq2 ⊢ ( 𝑘 = 0 → ( 𝑑 ↑𝑟 𝑘 ) = ( 𝑑 ↑𝑟 0 ) )
73 72 ssiun2s ⊢ ( 0 ∈ ℕ0 → ( 𝑑 ↑𝑟 0 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) )
74 71 73 ax-mp ⊢ ( 𝑑 ↑𝑟 0 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 )
75 1nn0 ⊢ 1 ∈ ℕ0
76 oveq2 ⊢ ( 𝑘 = 1 → ( 𝑑 ↑𝑟 𝑘 ) = ( 𝑑 ↑𝑟 1 ) )
77 76 ssiun2s ⊢ ( 1 ∈ ℕ0 → ( 𝑑 ↑𝑟 1 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) )
78 75 77 ax-mp ⊢ ( 𝑑 ↑𝑟 1 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 )
79 74 78 unssi ⊢ ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 )
80 70 79 eqsstri ⊢ ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 1 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 )
81 simpl ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ) → 𝑦 ∈ ℕ )
82 relexpsucnnr ⊢ ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ∈ V ∧ 𝑦 ∈ ℕ ) → ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ∘ ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ) )
83 68 81 82 sylancr ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ) → ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ∘ ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ) )
84 coss1 ⊢ ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) → ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ∘ ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ) ⊆ ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ) )
85 coundi ⊢ ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ) = ( ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 0 ) ) ∪ ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) )
86 relexp0g ⊢ ( 𝑑 ∈ V → ( 𝑑 ↑𝑟 0 ) = ( I ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) )
87 86 elv ⊢ ( 𝑑 ↑𝑟 0 ) = ( I ↾ ( dom 𝑑 ∪ ran 𝑑 ) )
88 87 coeq2i ⊢ ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 0 ) ) = ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( I ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) )
89 coiun1 ⊢ ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( I ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) ) = ∪ 𝑘 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( I ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) )
90 coires1 ⊢ ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( I ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) ) = ( ( 𝑑 ↑𝑟 𝑘 ) ↾ ( dom 𝑑 ∪ ran 𝑑 ) )
91 90 a1i ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( I ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) ) = ( ( 𝑑 ↑𝑟 𝑘 ) ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) )
92 91 iuneq2i ⊢ ∪ 𝑘 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( I ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) ) = ∪ 𝑘 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ↾ ( dom 𝑑 ∪ ran 𝑑 ) )
93 88 89 92 3eqtri ⊢ ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 0 ) ) = ∪ 𝑘 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ↾ ( dom 𝑑 ∪ ran 𝑑 ) )
94 ss2iun ⊢ ( ∀ 𝑘 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) ⊆ ( 𝑑 ↑𝑟 𝑘 ) → ∪ 𝑘 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) )
95 resss ⊢ ( ( 𝑑 ↑𝑟 𝑘 ) ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) ⊆ ( 𝑑 ↑𝑟 𝑘 )
96 95 a1i ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑑 ↑𝑟 𝑘 ) ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) ⊆ ( 𝑑 ↑𝑟 𝑘 ) )
97 94 96 mprg ⊢ ∪ 𝑘 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ↾ ( dom 𝑑 ∪ ran 𝑑 ) ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 )
98 93 97 eqsstri ⊢ ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 0 ) ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 )
99 coiun1 ⊢ ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) = ∪ 𝑘 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) )
100 iunss2 ⊢ ( ∀ 𝑘 ∈ ℕ0 ∃ 𝑖 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 𝑖 ) → ∪ 𝑘 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ∪ 𝑖 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑖 ) )
101 peano2nn0 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
102 sbcel1v ⊢ ( [ ( 𝑘 + 1 ) / 𝑖 ] 𝑖 ∈ ℕ0 ↔ ( 𝑘 + 1 ) ∈ ℕ0 )
103 101 102 sylibr ⊢ ( 𝑘 ∈ ℕ0 → [ ( 𝑘 + 1 ) / 𝑖 ] 𝑖 ∈ ℕ0 )
104 vex ⊢ 𝑑 ∈ V
105 relexpaddss ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 𝑑 ∈ V ) → ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 ( 𝑘 + 1 ) ) )
106 75 104 105 mp3an23 ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 ( 𝑘 + 1 ) ) )
107 ovex ⊢ ( 𝑘 + 1 ) ∈ V
108 csbconstg ⊢ ( ( 𝑘 + 1 ) ∈ V → ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) = ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) )
109 107 108 ax-mp ⊢ ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) = ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) )
110 csbov2g ⊢ ( ( 𝑘 + 1 ) ∈ V → ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ ( 𝑑 ↑𝑟 𝑖 ) = ( 𝑑 ↑𝑟 ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ 𝑖 ) )
111 csbvarg ⊢ ( ( 𝑘 + 1 ) ∈ V → ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ 𝑖 = ( 𝑘 + 1 ) )
112 111 oveq2d ⊢ ( ( 𝑘 + 1 ) ∈ V → ( 𝑑 ↑𝑟 ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ 𝑖 ) = ( 𝑑 ↑𝑟 ( 𝑘 + 1 ) ) )
113 110 112 eqtrd ⊢ ( ( 𝑘 + 1 ) ∈ V → ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ ( 𝑑 ↑𝑟 𝑖 ) = ( 𝑑 ↑𝑟 ( 𝑘 + 1 ) ) )
114 107 113 ax-mp ⊢ ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ ( 𝑑 ↑𝑟 𝑖 ) = ( 𝑑 ↑𝑟 ( 𝑘 + 1 ) )
115 106 109 114 3sstr4g ⊢ ( 𝑘 ∈ ℕ0 → ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ ( 𝑑 ↑𝑟 𝑖 ) )
116 sbcssg ⊢ ( ( 𝑘 + 1 ) ∈ V → ( [ ( 𝑘 + 1 ) / 𝑖 ] ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 𝑖 ) ↔ ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ ( 𝑑 ↑𝑟 𝑖 ) ) )
117 107 116 ax-mp ⊢ ( [ ( 𝑘 + 1 ) / 𝑖 ] ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 𝑖 ) ↔ ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ ( 𝑑 ↑𝑟 𝑖 ) )
118 115 117 sylibr ⊢ ( 𝑘 ∈ ℕ0 → [ ( 𝑘 + 1 ) / 𝑖 ] ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 𝑖 ) )
119 sbcan ⊢ ( [ ( 𝑘 + 1 ) / 𝑖 ] ( 𝑖 ∈ ℕ0 ∧ ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 𝑖 ) ) ↔ ( [ ( 𝑘 + 1 ) / 𝑖 ] 𝑖 ∈ ℕ0 ∧ [ ( 𝑘 + 1 ) / 𝑖 ] ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 𝑖 ) ) )
120 103 118 119 sylanbrc ⊢ ( 𝑘 ∈ ℕ0 → [ ( 𝑘 + 1 ) / 𝑖 ] ( 𝑖 ∈ ℕ0 ∧ ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 𝑖 ) ) )
121 120 spesbcd ⊢ ( 𝑘 ∈ ℕ0 → ∃ 𝑖 ( 𝑖 ∈ ℕ0 ∧ ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 𝑖 ) ) )
122 df-rex ⊢ ( ∃ 𝑖 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 𝑖 ) ↔ ∃ 𝑖 ( 𝑖 ∈ ℕ0 ∧ ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 𝑖 ) ) )
123 121 122 sylibr ⊢ ( 𝑘 ∈ ℕ0 → ∃ 𝑖 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ( 𝑑 ↑𝑟 𝑖 ) )
124 100 123 mprg ⊢ ∪ 𝑘 ∈ ℕ0 ( ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ∪ 𝑖 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑖 )
125 99 124 eqsstri ⊢ ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ∪ 𝑖 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑖 )
126 oveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑑 ↑𝑟 𝑖 ) = ( 𝑑 ↑𝑟 𝑘 ) )
127 126 cbviunv ⊢ ∪ 𝑖 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑖 ) = ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 )
128 125 127 sseqtri ⊢ ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 )
129 98 128 unssi ⊢ ( ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 0 ) ) ∪ ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( 𝑑 ↑𝑟 1 ) ) ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 )
130 85 129 eqsstri ⊢ ( ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ∘ ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 )
131 84 130 sstrdi ⊢ ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) → ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ∘ ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) )
132 131 adantl ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ) → ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ∘ ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) )
133 83 132 eqsstrd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ) → ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) )
134 133 ex ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) → ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) ) )
135 59 61 63 65 80 134 nnind ⊢ ( 𝑖 ∈ ℕ → ( ( ( 𝑑 ↑𝑟 0 ) ∪ ( 𝑑 ↑𝑟 1 ) ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) )
136 57 135 eqsstrid ⊢ ( 𝑖 ∈ ℕ → ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) )
137 47 136 mprgbir ⊢ ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 )
138 iuneq1 ⊢ ( ℕ0 = ( ℕ ∪ { 0 , 1 } ) → ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) = ∪ 𝑘 ∈ ( ℕ ∪ { 0 , 1 } ) ( 𝑑 ↑𝑟 𝑘 ) )
139 18 138 ax-mp ⊢ ∪ 𝑘 ∈ ℕ0 ( 𝑑 ↑𝑟 𝑘 ) = ∪ 𝑘 ∈ ( ℕ ∪ { 0 , 1 } ) ( 𝑑 ↑𝑟 𝑘 )
140 137 139 sseqtri ⊢ ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ( ℕ ∪ { 0 , 1 } ) ( 𝑑 ↑𝑟 𝑘 )
141 1 2 3 4 5 18 37 46 140 comptiunov2i ⊢ ( t+ ∘ r* ) = t*