Metamath Proof Explorer

Theorem cotrcltrcl

Description: The transitive closure is idempotent. (Contributed by RP, 16-Jun-2020)

Ref Expression
Assertion cotrcltrcl 
|- ( t+ o. t+ ) = t+

Proof

Step Hyp Ref Expression
1 dftrcl3 
 |-  t+ = ( a e. _V |-> U_ i e. NN ( a ^r i ) )
2 dftrcl3 
 |-  t+ = ( b e. _V |-> U_ j e. NN ( b ^r j ) )
3 dftrcl3 
 |-  t+ = ( c e. _V |-> U_ k e. NN ( c ^r k ) )
4 nnex 
 |-  NN e. _V
5 unidm 
 |-  ( NN u. NN ) = NN
6 5 eqcomi 
 |-  NN = ( NN u. NN )
7 1ex 
 |-  1 e. _V
8 oveq2 
 |-  ( i = 1 -> ( U_ j e. NN ( d ^r j ) ^r i ) = ( U_ j e. NN ( d ^r j ) ^r 1 ) )
9 7 8 iunxsn 
 |-  U_ i e. { 1 } ( U_ j e. NN ( d ^r j ) ^r i ) = ( U_ j e. NN ( d ^r j ) ^r 1 )
10 ovex 
 |-  ( d ^r j ) e. _V
11 4 10 iunex 
 |-  U_ j e. NN ( d ^r j ) e. _V
12 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 ) )
13 11 12 ax-mp 
 |-  ( U_ j e. NN ( d ^r j ) ^r 1 ) = U_ j e. NN ( d ^r j )
14 oveq2 
 |-  ( j = k -> ( d ^r j ) = ( d ^r k ) )
15 14 cbviunv 
 |-  U_ j e. NN ( d ^r j ) = U_ k e. NN ( d ^r k )
16 13 15 eqtri 
 |-  ( U_ j e. NN ( d ^r j ) ^r 1 ) = U_ k e. NN ( d ^r k )
17 9 16 eqtri 
 |-  U_ i e. { 1 } ( U_ j e. NN ( d ^r j ) ^r i ) = U_ k e. NN ( d ^r k )
18 17 eqcomi 
 |-  U_ k e. NN ( d ^r k ) = U_ i e. { 1 } ( U_ j e. NN ( d ^r j ) ^r i )
19 1nn 
 |-  1 e. NN
20 snssi 
 |-  ( 1 e. NN -> { 1 } C_ NN )
21 iunss1 
 |-  ( { 1 } C_ NN -> U_ i e. { 1 } ( U_ j e. NN ( d ^r j ) ^r i ) C_ U_ i e. NN ( U_ j e. NN ( d ^r j ) ^r i ) )
22 19 20 21 mp2b 
 |-  U_ i e. { 1 } ( U_ j e. NN ( d ^r j ) ^r i ) C_ U_ i e. NN ( U_ j e. NN ( d ^r j ) ^r i )
23 18 22 eqsstri 
 |-  U_ k e. NN ( d ^r k ) C_ U_ i e. NN ( U_ j e. NN ( d ^r j ) ^r i )
24 iunss 
 |-  ( U_ i e. NN ( U_ j e. NN ( d ^r j ) ^r i ) C_ U_ k e. NN ( d ^r k ) <-> A. i e. NN ( U_ j e. NN ( d ^r j ) ^r i ) C_ U_ k e. NN ( d ^r k ) )
25 oveq2 
 |-  ( x = 1 -> ( U_ j e. NN ( d ^r j ) ^r x ) = ( U_ j e. NN ( d ^r j ) ^r 1 ) )
26 25 sseq1d 
 |-  ( x = 1 -> ( ( U_ j e. NN ( d ^r j ) ^r x ) C_ U_ k e. NN ( d ^r k ) <-> ( U_ j e. NN ( d ^r j ) ^r 1 ) C_ U_ k e. NN ( d ^r k ) ) )
27 oveq2 
 |-  ( x = y -> ( U_ j e. NN ( d ^r j ) ^r x ) = ( U_ j e. NN ( d ^r j ) ^r y ) )
28 27 sseq1d 
 |-  ( x = y -> ( ( U_ j e. NN ( d ^r j ) ^r x ) C_ U_ k e. NN ( d ^r k ) <-> ( U_ j e. NN ( d ^r j ) ^r y ) C_ U_ k e. NN ( d ^r k ) ) )
29 oveq2 
 |-  ( x = ( y + 1 ) -> ( U_ j e. NN ( d ^r j ) ^r x ) = ( U_ j e. NN ( d ^r j ) ^r ( y + 1 ) ) )
30 29 sseq1d 
 |-  ( x = ( y + 1 ) -> ( ( U_ j e. NN ( d ^r j ) ^r x ) C_ U_ k e. NN ( d ^r k ) <-> ( U_ j e. NN ( d ^r j ) ^r ( y + 1 ) ) C_ U_ k e. NN ( d ^r k ) ) )
31 oveq2 
 |-  ( x = i -> ( U_ j e. NN ( d ^r j ) ^r x ) = ( U_ j e. NN ( d ^r j ) ^r i ) )
32 31 sseq1d 
 |-  ( x = i -> ( ( U_ j e. NN ( d ^r j ) ^r x ) C_ U_ k e. NN ( d ^r k ) <-> ( U_ j e. NN ( d ^r j ) ^r i ) C_ U_ k e. NN ( d ^r k ) ) )
33 16 eqimssi 
 |-  ( U_ j e. NN ( d ^r j ) ^r 1 ) C_ U_ k e. NN ( d ^r k )
34 simpl 
 |-  ( ( y e. NN /\ ( U_ j e. NN ( d ^r j ) ^r y ) C_ U_ k e. NN ( d ^r k ) ) -> y e. NN )
35 relexpsucnnr 
 |-  ( ( U_ j e. NN ( d ^r j ) e. _V /\ y e. NN ) -> ( U_ j e. NN ( d ^r j ) ^r ( y + 1 ) ) = ( ( U_ j e. NN ( d ^r j ) ^r y ) o. U_ j e. NN ( d ^r j ) ) )
36 11 34 35 sylancr 
 |-  ( ( y e. NN /\ ( U_ j e. NN ( d ^r j ) ^r y ) C_ U_ k e. NN ( d ^r k ) ) -> ( U_ j e. NN ( d ^r j ) ^r ( y + 1 ) ) = ( ( U_ j e. NN ( d ^r j ) ^r y ) o. U_ j e. NN ( d ^r j ) ) )
37 coss1 
 |-  ( ( U_ j e. NN ( d ^r j ) ^r y ) C_ U_ k e. NN ( d ^r k ) -> ( ( U_ j e. NN ( d ^r j ) ^r y ) o. U_ j e. NN ( d ^r j ) ) C_ ( U_ k e. NN ( d ^r k ) o. U_ j e. NN ( d ^r j ) ) )
38 37 adantl 
 |-  ( ( y e. NN /\ ( U_ j e. NN ( d ^r j ) ^r y ) C_ U_ k e. NN ( d ^r k ) ) -> ( ( U_ j e. NN ( d ^r j ) ^r y ) o. U_ j e. NN ( d ^r j ) ) C_ ( U_ k e. NN ( d ^r k ) o. U_ j e. NN ( d ^r j ) ) )
39 15 coeq2i 
 |-  ( U_ k e. NN ( d ^r k ) o. U_ j e. NN ( d ^r j ) ) = ( U_ k e. NN ( d ^r k ) o. U_ k e. NN ( d ^r k ) )
40 trclfvcotrg 
 |-  ( ( t+ ` d ) o. ( t+ ` d ) ) C_ ( t+ ` d )
41 oveq1 
 |-  ( c = d -> ( c ^r k ) = ( d ^r k ) )
42 41 iuneq2d 
 |-  ( c = d -> U_ k e. NN ( c ^r k ) = U_ k e. NN ( d ^r k ) )
43 ovex 
 |-  ( d ^r k ) e. _V
44 4 43 iunex 
 |-  U_ k e. NN ( d ^r k ) e. _V
45 42 3 44 fvmpt 
 |-  ( d e. _V -> ( t+ ` d ) = U_ k e. NN ( d ^r k ) )
46 45 elv 
 |-  ( t+ ` d ) = U_ k e. NN ( d ^r k )
47 46 46 coeq12i 
 |-  ( ( t+ ` d ) o. ( t+ ` d ) ) = ( U_ k e. NN ( d ^r k ) o. U_ k e. NN ( d ^r k ) )
48 40 47 46 3sstr3i 
 |-  ( U_ k e. NN ( d ^r k ) o. U_ k e. NN ( d ^r k ) ) C_ U_ k e. NN ( d ^r k )
49 39 48 eqsstri 
 |-  ( U_ k e. NN ( d ^r k ) o. U_ j e. NN ( d ^r j ) ) C_ U_ k e. NN ( d ^r k )
50 38 49 sstrdi 
 |-  ( ( y e. NN /\ ( U_ j e. NN ( d ^r j ) ^r y ) C_ U_ k e. NN ( d ^r k ) ) -> ( ( U_ j e. NN ( d ^r j ) ^r y ) o. U_ j e. NN ( d ^r j ) ) C_ U_ k e. NN ( d ^r k ) )
51 36 50 eqsstrd 
 |-  ( ( y e. NN /\ ( U_ j e. NN ( d ^r j ) ^r y ) C_ U_ k e. NN ( d ^r k ) ) -> ( U_ j e. NN ( d ^r j ) ^r ( y + 1 ) ) C_ U_ k e. NN ( d ^r k ) )
52 51 ex 
 |-  ( y e. NN -> ( ( U_ j e. NN ( d ^r j ) ^r y ) C_ U_ k e. NN ( d ^r k ) -> ( U_ j e. NN ( d ^r j ) ^r ( y + 1 ) ) C_ U_ k e. NN ( d ^r k ) ) )
53 26 28 30 32 33 52 nnind 
 |-  ( i e. NN -> ( U_ j e. NN ( d ^r j ) ^r i ) C_ U_ k e. NN ( d ^r k ) )
54 24 53 mprgbir 
 |-  U_ i e. NN ( U_ j e. NN ( d ^r j ) ^r i ) C_ U_ k e. NN ( d ^r k )
55 iuneq1 
 |-  ( NN = ( NN u. NN ) -> U_ k e. NN ( d ^r k ) = U_ k e. ( NN u. NN ) ( d ^r k ) )
56 6 55 ax-mp 
 |-  U_ k e. NN ( d ^r k ) = U_ k e. ( NN u. NN ) ( d ^r k )
57 54 56 sseqtri 
 |-  U_ i e. NN ( U_ j e. NN ( d ^r j ) ^r i ) C_ U_ k e. ( NN u. NN ) ( d ^r k )
58 1 2 3 4 4 6 23 23 57 comptiunov2i 
 |-  ( t+ o. t+ ) = t+