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+ o. r* ) = t*

Proof

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