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

Proof

Step Hyp Ref Expression
1 dfrcl4 
 |-  r* = ( a e. _V |-> U_ i e. { 0 , 1 } ( a ^r i ) )
2 dftrcl3 
 |-  t+ = ( b e. _V |-> U_ j e. NN ( b ^r j ) )
3 dfrtrcl3 
 |-  t* = ( c e. _V |-> U_ k e. NN0 ( c ^r k ) )
4 prex 
 |-  { 0 , 1 } e. _V
5 nnex 
 |-  NN e. _V
6 df-n0 
 |-  NN0 = ( NN u. { 0 } )
7 uncom 
 |-  ( NN u. { 0 } ) = ( { 0 } u. NN )
8 df-pr 
 |-  { 0 , 1 } = ( { 0 } u. { 1 } )
9 8 uneq1i 
 |-  ( { 0 , 1 } u. NN ) = ( ( { 0 } u. { 1 } ) u. NN )
10 unass 
 |-  ( ( { 0 } u. { 1 } ) u. NN ) = ( { 0 } u. ( { 1 } u. NN ) )
11 1nn 
 |-  1 e. NN
12 snssi 
 |-  ( 1 e. NN -> { 1 } C_ NN )
13 11 12 ax-mp 
 |-  { 1 } C_ NN
14 ssequn1 
 |-  ( { 1 } C_ NN <-> ( { 1 } u. NN ) = NN )
15 13 14 mpbi 
 |-  ( { 1 } u. NN ) = NN
16 15 uneq2i 
 |-  ( { 0 } u. ( { 1 } u. NN ) ) = ( { 0 } u. NN )
17 9 10 16 3eqtrri 
 |-  ( { 0 } u. NN ) = ( { 0 , 1 } u. NN )
18 6 7 17 3eqtri 
 |-  NN0 = ( { 0 , 1 } u. NN )
19 oveq2 
 |-  ( k = i -> ( d ^r k ) = ( d ^r i ) )
20 19 cbviunv 
 |-  U_ k e. { 0 , 1 } ( d ^r k ) = U_ i e. { 0 , 1 } ( d ^r i )
21 ss2iun 
 |-  ( A. i e. { 0 , 1 } ( d ^r i ) C_ ( U_ j e. NN ( d ^r j ) ^r i ) -> U_ i e. { 0 , 1 } ( d ^r i ) C_ U_ i e. { 0 , 1 } ( U_ j e. NN ( d ^r j ) ^r i ) )
22 relexp1g 
 |-  ( d e. _V -> ( d ^r 1 ) = d )
23 22 elv 
 |-  ( d ^r 1 ) = d
24 oveq2 
 |-  ( j = 1 -> ( d ^r j ) = ( d ^r 1 ) )
25 24 ssiun2s 
 |-  ( 1 e. NN -> ( d ^r 1 ) C_ U_ j e. NN ( d ^r j ) )
26 11 25 ax-mp 
 |-  ( d ^r 1 ) C_ U_ j e. NN ( d ^r j )
27 23 26 eqsstrri 
 |-  d C_ U_ j e. NN ( d ^r j )
28 27 a1i 
 |-  ( i e. { 0 , 1 } -> d C_ U_ j e. NN ( d ^r j ) )
29 ovex 
 |-  ( d ^r j ) e. _V
30 5 29 iunex 
 |-  U_ j e. NN ( d ^r j ) e. _V
31 30 a1i 
 |-  ( i e. { 0 , 1 } -> U_ j e. NN ( d ^r j ) e. _V )
32 0nn0 
 |-  0 e. NN0
33 1nn0 
 |-  1 e. NN0
34 prssi 
 |-  ( ( 0 e. NN0 /\ 1 e. NN0 ) -> { 0 , 1 } C_ NN0 )
35 32 33 34 mp2an 
 |-  { 0 , 1 } C_ NN0
36 35 sseli 
 |-  ( i e. { 0 , 1 } -> i e. NN0 )
37 28 31 36 relexpss1d 
 |-  ( i e. { 0 , 1 } -> ( d ^r i ) C_ ( U_ j e. NN ( d ^r j ) ^r i ) )
38 21 37 mprg 
 |-  U_ i e. { 0 , 1 } ( d ^r i ) C_ U_ i e. { 0 , 1 } ( U_ j e. NN ( d ^r j ) ^r i )
39 20 38 eqsstri 
 |-  U_ k e. { 0 , 1 } ( d ^r k ) C_ U_ i e. { 0 , 1 } ( U_ j e. NN ( d ^r j ) ^r i )
40 oveq2 
 |-  ( k = j -> ( d ^r k ) = ( d ^r j ) )
41 40 cbviunv 
 |-  U_ k e. NN ( d ^r k ) = U_ j e. NN ( d ^r j )
42 relexp1g 
 |-  ( U_ j e. NN ( d ^r j ) e. _V -> ( U_ j e. NN ( d ^r j ) ^r 1 ) = U_ j e. NN ( d ^r j ) )
43 30 42 ax-mp 
 |-  ( U_ j e. NN ( d ^r j ) ^r 1 ) = U_ j e. NN ( d ^r j )
44 41 43 eqtr4i 
 |-  U_ k e. NN ( d ^r k ) = ( U_ j e. NN ( d ^r j ) ^r 1 )
45 1elpr01 
 |-  1 e. { 0 , 1 }
46 oveq2 
 |-  ( i = 1 -> ( U_ j e. NN ( d ^r j ) ^r i ) = ( U_ j e. NN ( d ^r j ) ^r 1 ) )
47 46 ssiun2s 
 |-  ( 1 e. { 0 , 1 } -> ( U_ j e. NN ( d ^r j ) ^r 1 ) C_ U_ i e. { 0 , 1 } ( U_ j e. NN ( d ^r j ) ^r i ) )
48 45 47 ax-mp 
 |-  ( U_ j e. NN ( d ^r j ) ^r 1 ) C_ U_ i e. { 0 , 1 } ( U_ j e. NN ( d ^r j ) ^r i )
49 44 48 eqsstri 
 |-  U_ k e. NN ( d ^r k ) C_ U_ i e. { 0 , 1 } ( U_ j e. NN ( d ^r j ) ^r i )
50 c0ex 
 |-  0 e. _V
51 50 prid1 
 |-  0 e. { 0 , 1 }
52 oveq2 
 |-  ( k = 0 -> ( d ^r k ) = ( d ^r 0 ) )
53 52 ssiun2s 
 |-  ( 0 e. { 0 , 1 } -> ( d ^r 0 ) C_ U_ k e. { 0 , 1 } ( d ^r k ) )
54 51 53 ax-mp 
 |-  ( d ^r 0 ) C_ U_ k e. { 0 , 1 } ( d ^r k )
55 ssid 
 |-  U_ k e. NN ( d ^r k ) C_ U_ k e. NN ( d ^r k )
56 unss12 
 |-  ( ( ( d ^r 0 ) C_ U_ k e. { 0 , 1 } ( d ^r k ) /\ U_ k e. NN ( d ^r k ) C_ U_ k e. NN ( d ^r k ) ) -> ( ( d ^r 0 ) u. U_ k e. NN ( d ^r k ) ) C_ ( U_ k e. { 0 , 1 } ( d ^r k ) u. U_ k e. NN ( d ^r k ) ) )
57 54 55 56 mp2an 
 |-  ( ( d ^r 0 ) u. U_ k e. NN ( d ^r k ) ) C_ ( U_ k e. { 0 , 1 } ( d ^r k ) u. U_ k e. NN ( d ^r k ) )
58 iuneq1 
 |-  ( { 0 , 1 } = ( { 0 } u. { 1 } ) -> U_ i e. { 0 , 1 } ( U_ j e. NN ( d ^r j ) ^r i ) = U_ i e. ( { 0 } u. { 1 } ) ( U_ j e. NN ( d ^r j ) ^r i ) )
59 8 58 ax-mp 
 |-  U_ i e. { 0 , 1 } ( U_ j e. NN ( d ^r j ) ^r i ) = U_ i e. ( { 0 } u. { 1 } ) ( U_ j e. NN ( d ^r j ) ^r i )
60 iunxun 
 |-  U_ i e. ( { 0 } u. { 1 } ) ( U_ j e. NN ( d ^r j ) ^r i ) = ( U_ i e. { 0 } ( U_ j e. NN ( d ^r j ) ^r i ) u. U_ i e. { 1 } ( U_ j e. NN ( d ^r j ) ^r i ) )
61 oveq2 
 |-  ( i = 0 -> ( U_ j e. NN ( d ^r j ) ^r i ) = ( U_ j e. NN ( d ^r j ) ^r 0 ) )
62 50 61 iunxsn 
 |-  U_ i e. { 0 } ( U_ j e. NN ( d ^r j ) ^r i ) = ( U_ j e. NN ( d ^r j ) ^r 0 )
63 vex 
 |-  d e. _V
64 nnssnn0 
 |-  NN C_ NN0
65 inelcm 
 |-  ( ( 1 e. { 0 , 1 } /\ 1 e. NN ) -> ( { 0 , 1 } i^i NN ) =/= (/) )
66 45 11 65 mp2an 
 |-  ( { 0 , 1 } i^i NN ) =/= (/)
67 iunrelexp0 
 |-  ( ( d e. _V /\ NN C_ NN0 /\ ( { 0 , 1 } i^i NN ) =/= (/) ) -> ( U_ j e. NN ( d ^r j ) ^r 0 ) = ( d ^r 0 ) )
68 63 64 66 67 mp3an 
 |-  ( U_ j e. NN ( d ^r j ) ^r 0 ) = ( d ^r 0 )
69 62 68 eqtri 
 |-  U_ i e. { 0 } ( U_ j e. NN ( d ^r j ) ^r i ) = ( d ^r 0 )
70 1ex 
 |-  1 e. _V
71 70 46 iunxsn 
 |-  U_ i e. { 1 } ( U_ j e. NN ( d ^r j ) ^r i ) = ( U_ j e. NN ( d ^r j ) ^r 1 )
72 43 41 eqtr4i 
 |-  ( U_ j e. NN ( d ^r j ) ^r 1 ) = U_ k e. NN ( d ^r k )
73 71 72 eqtri 
 |-  U_ i e. { 1 } ( U_ j e. NN ( d ^r j ) ^r i ) = U_ k e. NN ( d ^r k )
74 69 73 uneq12i 
 |-  ( U_ i e. { 0 } ( U_ j e. NN ( d ^r j ) ^r i ) u. U_ i e. { 1 } ( U_ j e. NN ( d ^r j ) ^r i ) ) = ( ( d ^r 0 ) u. U_ k e. NN ( d ^r k ) )
75 59 60 74 3eqtri 
 |-  U_ i e. { 0 , 1 } ( U_ j e. NN ( d ^r j ) ^r i ) = ( ( d ^r 0 ) u. U_ k e. NN ( d ^r k ) )
76 iunxun 
 |-  U_ k e. ( { 0 , 1 } u. NN ) ( d ^r k ) = ( U_ k e. { 0 , 1 } ( d ^r k ) u. U_ k e. NN ( d ^r k ) )
77 57 75 76 3sstr4i 
 |-  U_ i e. { 0 , 1 } ( U_ j e. NN ( d ^r j ) ^r i ) C_ U_ k e. ( { 0 , 1 } u. NN ) ( d ^r k )
78 1 2 3 4 5 18 39 49 77 comptiunov2i 
 |-  ( r* o. t+ ) = t*