Metamath Proof Explorer

Theorem trclfvdecomr

Description: The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020)

Ref Expression
Assertion trclfvdecomr 
|- ( R e. V -> ( t+ ` R ) = ( R u. ( ( t+ ` R ) o. R ) ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( R e. V -> R e. _V )
2 oveq1 
 |-  ( r = R -> ( r ^r n ) = ( R ^r n ) )
3 2 iuneq2d 
 |-  ( r = R -> U_ n e. NN ( r ^r n ) = U_ n e. NN ( R ^r n ) )
4 dftrcl3 
 |-  t+ = ( r e. _V |-> U_ n e. NN ( r ^r n ) )
5 nnex 
 |-  NN e. _V
6 ovex 
 |-  ( R ^r n ) e. _V
7 5 6 iunex 
 |-  U_ n e. NN ( R ^r n ) e. _V
8 3 4 7 fvmpt 
 |-  ( R e. _V -> ( t+ ` R ) = U_ n e. NN ( R ^r n ) )
9 1 8 syl 
 |-  ( R e. V -> ( t+ ` R ) = U_ n e. NN ( R ^r n ) )
10 nnuz 
 |-  NN = ( ZZ>= ` 1 )
11 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
12 uzsplit 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> ( ZZ>= ` 1 ) = ( ( 1 ... ( 2 - 1 ) ) u. ( ZZ>= ` 2 ) ) )
13 11 12 ax-mp 
 |-  ( ZZ>= ` 1 ) = ( ( 1 ... ( 2 - 1 ) ) u. ( ZZ>= ` 2 ) )
14 2m1e1 
 |-  ( 2 - 1 ) = 1
15 14 oveq2i 
 |-  ( 1 ... ( 2 - 1 ) ) = ( 1 ... 1 )
16 1z 
 |-  1 e. ZZ
17 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
18 16 17 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
19 15 18 eqtri 
 |-  ( 1 ... ( 2 - 1 ) ) = { 1 }
20 19 uneq1i 
 |-  ( ( 1 ... ( 2 - 1 ) ) u. ( ZZ>= ` 2 ) ) = ( { 1 } u. ( ZZ>= ` 2 ) )
21 10 13 20 3eqtri 
 |-  NN = ( { 1 } u. ( ZZ>= ` 2 ) )
22 iuneq1 
 |-  ( NN = ( { 1 } u. ( ZZ>= ` 2 ) ) -> U_ n e. NN ( R ^r n ) = U_ n e. ( { 1 } u. ( ZZ>= ` 2 ) ) ( R ^r n ) )
23 21 22 ax-mp 
 |-  U_ n e. NN ( R ^r n ) = U_ n e. ( { 1 } u. ( ZZ>= ` 2 ) ) ( R ^r n )
24 iunxun 
 |-  U_ n e. ( { 1 } u. ( ZZ>= ` 2 ) ) ( R ^r n ) = ( U_ n e. { 1 } ( R ^r n ) u. U_ n e. ( ZZ>= ` 2 ) ( R ^r n ) )
25 1ex 
 |-  1 e. _V
26 oveq2 
 |-  ( n = 1 -> ( R ^r n ) = ( R ^r 1 ) )
27 25 26 iunxsn 
 |-  U_ n e. { 1 } ( R ^r n ) = ( R ^r 1 )
28 27 uneq1i 
 |-  ( U_ n e. { 1 } ( R ^r n ) u. U_ n e. ( ZZ>= ` 2 ) ( R ^r n ) ) = ( ( R ^r 1 ) u. U_ n e. ( ZZ>= ` 2 ) ( R ^r n ) )
29 23 24 28 3eqtri 
 |-  U_ n e. NN ( R ^r n ) = ( ( R ^r 1 ) u. U_ n e. ( ZZ>= ` 2 ) ( R ^r n ) )
30 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
31 oveq1 
 |-  ( r = R -> ( r ^r m ) = ( R ^r m ) )
32 31 iuneq2d 
 |-  ( r = R -> U_ m e. NN ( r ^r m ) = U_ m e. NN ( R ^r m ) )
33 dftrcl3 
 |-  t+ = ( r e. _V |-> U_ m e. NN ( r ^r m ) )
34 ovex 
 |-  ( R ^r m ) e. _V
35 5 34 iunex 
 |-  U_ m e. NN ( R ^r m ) e. _V
36 32 33 35 fvmpt 
 |-  ( R e. _V -> ( t+ ` R ) = U_ m e. NN ( R ^r m ) )
37 1 36 syl 
 |-  ( R e. V -> ( t+ ` R ) = U_ m e. NN ( R ^r m ) )
38 37 coeq1d 
 |-  ( R e. V -> ( ( t+ ` R ) o. R ) = ( U_ m e. NN ( R ^r m ) o. R ) )
39 coiun1 
 |-  ( U_ m e. NN ( R ^r m ) o. R ) = U_ m e. NN ( ( R ^r m ) o. R )
40 uz2m1nn 
 |-  ( n e. ( ZZ>= ` 2 ) -> ( n - 1 ) e. NN )
41 40 adantl 
 |-  ( ( R e. V /\ n e. ( ZZ>= ` 2 ) ) -> ( n - 1 ) e. NN )
42 eluzp1p1 
 |-  ( m e. ( ZZ>= ` 1 ) -> ( m + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
43 42 10 eleq2s 
 |-  ( m e. NN -> ( m + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
44 1p1e2 
 |-  ( 1 + 1 ) = 2
45 44 fveq2i 
 |-  ( ZZ>= ` ( 1 + 1 ) ) = ( ZZ>= ` 2 )
46 43 45 eleqtrdi 
 |-  ( m e. NN -> ( m + 1 ) e. ( ZZ>= ` 2 ) )
47 46 adantl 
 |-  ( ( R e. V /\ m e. NN ) -> ( m + 1 ) e. ( ZZ>= ` 2 ) )
48 oveq2 
 |-  ( m = ( n - 1 ) -> ( R ^r m ) = ( R ^r ( n - 1 ) ) )
49 48 coeq1d 
 |-  ( m = ( n - 1 ) -> ( ( R ^r m ) o. R ) = ( ( R ^r ( n - 1 ) ) o. R ) )
50 49 3ad2ant3 
 |-  ( ( R e. V /\ n e. ( ZZ>= ` 2 ) /\ m = ( n - 1 ) ) -> ( ( R ^r m ) o. R ) = ( ( R ^r ( n - 1 ) ) o. R ) )
51 oveq2 
 |-  ( n = ( m + 1 ) -> ( R ^r n ) = ( R ^r ( m + 1 ) ) )
52 51 3ad2ant3 
 |-  ( ( R e. V /\ m e. NN /\ n = ( m + 1 ) ) -> ( R ^r n ) = ( R ^r ( m + 1 ) ) )
53 relexpsucnnr 
 |-  ( ( R e. V /\ m e. NN ) -> ( R ^r ( m + 1 ) ) = ( ( R ^r m ) o. R ) )
54 53 eqcomd 
 |-  ( ( R e. V /\ m e. NN ) -> ( ( R ^r m ) o. R ) = ( R ^r ( m + 1 ) ) )
55 relexpsucnnr 
 |-  ( ( R e. V /\ ( n - 1 ) e. NN ) -> ( R ^r ( ( n - 1 ) + 1 ) ) = ( ( R ^r ( n - 1 ) ) o. R ) )
56 40 55 sylan2 
 |-  ( ( R e. V /\ n e. ( ZZ>= ` 2 ) ) -> ( R ^r ( ( n - 1 ) + 1 ) ) = ( ( R ^r ( n - 1 ) ) o. R ) )
57 eluzelcn 
 |-  ( n e. ( ZZ>= ` 2 ) -> n e. CC )
58 npcan1 
 |-  ( n e. CC -> ( ( n - 1 ) + 1 ) = n )
59 oveq2 
 |-  ( ( ( n - 1 ) + 1 ) = n -> ( R ^r ( ( n - 1 ) + 1 ) ) = ( R ^r n ) )
60 57 58 59 3syl 
 |-  ( n e. ( ZZ>= ` 2 ) -> ( R ^r ( ( n - 1 ) + 1 ) ) = ( R ^r n ) )
61 60 eqeq1d 
 |-  ( n e. ( ZZ>= ` 2 ) -> ( ( R ^r ( ( n - 1 ) + 1 ) ) = ( ( R ^r ( n - 1 ) ) o. R ) <-> ( R ^r n ) = ( ( R ^r ( n - 1 ) ) o. R ) ) )
62 61 adantl 
 |-  ( ( R e. V /\ n e. ( ZZ>= ` 2 ) ) -> ( ( R ^r ( ( n - 1 ) + 1 ) ) = ( ( R ^r ( n - 1 ) ) o. R ) <-> ( R ^r n ) = ( ( R ^r ( n - 1 ) ) o. R ) ) )
63 56 62 mpbid 
 |-  ( ( R e. V /\ n e. ( ZZ>= ` 2 ) ) -> ( R ^r n ) = ( ( R ^r ( n - 1 ) ) o. R ) )
64 41 47 50 52 54 63 cbviuneq12dv 
 |-  ( R e. V -> U_ m e. NN ( ( R ^r m ) o. R ) = U_ n e. ( ZZ>= ` 2 ) ( R ^r n ) )
65 39 64 syl5eq 
 |-  ( R e. V -> ( U_ m e. NN ( R ^r m ) o. R ) = U_ n e. ( ZZ>= ` 2 ) ( R ^r n ) )
66 38 65 eqtrd 
 |-  ( R e. V -> ( ( t+ ` R ) o. R ) = U_ n e. ( ZZ>= ` 2 ) ( R ^r n ) )
67 66 eqcomd 
 |-  ( R e. V -> U_ n e. ( ZZ>= ` 2 ) ( R ^r n ) = ( ( t+ ` R ) o. R ) )
68 30 67 uneq12d 
 |-  ( R e. V -> ( ( R ^r 1 ) u. U_ n e. ( ZZ>= ` 2 ) ( R ^r n ) ) = ( R u. ( ( t+ ` R ) o. R ) ) )
69 29 68 syl5eq 
 |-  ( R e. V -> U_ n e. NN ( R ^r n ) = ( R u. ( ( t+ ` R ) o. R ) ) )
70 9 69 eqtrd 
 |-  ( R e. V -> ( t+ ` R ) = ( R u. ( ( t+ ` R ) o. R ) ) )