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 1ex 
 |-  1 e. _V
46 45 prid2 
 |-  1 e. { 0 , 1 }
47 oveq2 
 |-  ( i = 1 -> ( U_ j e. NN ( d ^r j ) ^r i ) = ( U_ j e. NN ( d ^r j ) ^r 1 ) )
48 47 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 ) )
49 46 48 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 )
50 44 49 eqsstri 
 |-  U_ k e. NN ( d ^r k ) C_ U_ i e. { 0 , 1 } ( U_ j e. NN ( d ^r j ) ^r i )
51 c0ex 
 |-  0 e. _V
52 51 prid1 
 |-  0 e. { 0 , 1 }
53 oveq2 
 |-  ( k = 0 -> ( d ^r k ) = ( d ^r 0 ) )
54 53 ssiun2s 
 |-  ( 0 e. { 0 , 1 } -> ( d ^r 0 ) C_ U_ k e. { 0 , 1 } ( d ^r k ) )
55 52 54 ax-mp 
 |-  ( d ^r 0 ) C_ U_ k e. { 0 , 1 } ( d ^r k )
56 ssid 
 |-  U_ k e. NN ( d ^r k ) C_ U_ k e. NN ( d ^r k )
57 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 ) ) )
58 55 56 57 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 ) )
59 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 ) )
60 8 59 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 )
61 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 ) )
62 oveq2 
 |-  ( i = 0 -> ( U_ j e. NN ( d ^r j ) ^r i ) = ( U_ j e. NN ( d ^r j ) ^r 0 ) )
63 51 62 iunxsn 
 |-  U_ i e. { 0 } ( U_ j e. NN ( d ^r j ) ^r i ) = ( U_ j e. NN ( d ^r j ) ^r 0 )
64 vex 
 |-  d e. _V
65 nnssnn0 
 |-  NN C_ NN0
66 inelcm 
 |-  ( ( 1 e. { 0 , 1 } /\ 1 e. NN ) -> ( { 0 , 1 } i^i NN ) =/= (/) )
67 46 11 66 mp2an 
 |-  ( { 0 , 1 } i^i NN ) =/= (/)
68 iunrelexp0 
 |-  ( ( d e. _V /\ NN C_ NN0 /\ ( { 0 , 1 } i^i NN ) =/= (/) ) -> ( U_ j e. NN ( d ^r j ) ^r 0 ) = ( d ^r 0 ) )
69 64 65 67 68 mp3an 
 |-  ( U_ j e. NN ( d ^r j ) ^r 0 ) = ( d ^r 0 )
70 63 69 eqtri 
 |-  U_ i e. { 0 } ( U_ j e. NN ( d ^r j ) ^r i ) = ( d ^r 0 )
71 45 47 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 70 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 60 61 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 58 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 50 77 comptiunov2i 
 |-  ( r* o. t+ ) = t*