Metamath Proof Explorer

Theorem dftrcl3

Description: Transitive closure of a relation, expressed as indexed union of powers of relations. (Contributed by RP, 5-Jun-2020)

Ref Expression
Assertion dftrcl3 
|- t+ = ( r e. _V |-> U_ n e. NN ( r ^r n ) )

Proof

Step Hyp Ref Expression
1 df-trcl 
 |-  t+ = ( r e. _V |-> |^| { z | ( r C_ z /\ ( z o. z ) C_ z ) } )
2 relexp1g 
 |-  ( r e. _V -> ( r ^r 1 ) = r )
3 nnex 
 |-  NN e. _V
4 1nn 
 |-  1 e. NN
5 oveq1 
 |-  ( a = t -> ( a ^r n ) = ( t ^r n ) )
6 5 iuneq2d 
 |-  ( a = t -> U_ n e. NN ( a ^r n ) = U_ n e. NN ( t ^r n ) )
7 oveq2 
 |-  ( n = k -> ( t ^r n ) = ( t ^r k ) )
8 7 cbviunv 
 |-  U_ n e. NN ( t ^r n ) = U_ k e. NN ( t ^r k )
9 6 8 eqtrdi 
 |-  ( a = t -> U_ n e. NN ( a ^r n ) = U_ k e. NN ( t ^r k ) )
10 9 cbvmptv 
 |-  ( a e. _V |-> U_ n e. NN ( a ^r n ) ) = ( t e. _V |-> U_ k e. NN ( t ^r k ) )
11 10 ov2ssiunov2 
 |-  ( ( r e. _V /\ NN e. _V /\ 1 e. NN ) -> ( r ^r 1 ) C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) )
12 3 4 11 mp3an23 
 |-  ( r e. _V -> ( r ^r 1 ) C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) )
13 2 12 eqsstrrd 
 |-  ( r e. _V -> r C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) )
14 nnuz 
 |-  NN = ( ZZ>= ` 1 )
15 1nn0 
 |-  1 e. NN0
16 10 iunrelexpuztr 
 |-  ( ( r e. _V /\ NN = ( ZZ>= ` 1 ) /\ 1 e. NN0 ) -> ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) )
17 14 15 16 mp3an23 
 |-  ( r e. _V -> ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) )
18 fvex 
 |-  ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) e. _V
19 trcleq2lem 
 |-  ( z = ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) -> ( ( r C_ z /\ ( z o. z ) C_ z ) <-> ( r C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) /\ ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) ) )
20 19 a1i 
 |-  ( r e. _V -> ( z = ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) -> ( ( r C_ z /\ ( z o. z ) C_ z ) <-> ( r C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) /\ ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) ) ) )
21 20 alrimiv 
 |-  ( r e. _V -> A. z ( z = ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) -> ( ( r C_ z /\ ( z o. z ) C_ z ) <-> ( r C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) /\ ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) ) ) )
22 elabgt 
 |-  ( ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) e. _V /\ A. z ( z = ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) -> ( ( r C_ z /\ ( z o. z ) C_ z ) <-> ( r C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) /\ ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) ) ) ) -> ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) e. { z | ( r C_ z /\ ( z o. z ) C_ z ) } <-> ( r C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) /\ ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) ) )
23 18 21 22 sylancr 
 |-  ( r e. _V -> ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) e. { z | ( r C_ z /\ ( z o. z ) C_ z ) } <-> ( r C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) /\ ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) ) ) )
24 13 17 23 mpbir2and 
 |-  ( r e. _V -> ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) e. { z | ( r C_ z /\ ( z o. z ) C_ z ) } )
25 intss1 
 |-  ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) e. { z | ( r C_ z /\ ( z o. z ) C_ z ) } -> |^| { z | ( r C_ z /\ ( z o. z ) C_ z ) } C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) )
26 24 25 syl 
 |-  ( r e. _V -> |^| { z | ( r C_ z /\ ( z o. z ) C_ z ) } C_ ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) )
27 vex 
 |-  s e. _V
28 trcleq2lem 
 |-  ( z = s -> ( ( r C_ z /\ ( z o. z ) C_ z ) <-> ( r C_ s /\ ( s o. s ) C_ s ) ) )
29 27 28 elab 
 |-  ( s e. { z | ( r C_ z /\ ( z o. z ) C_ z ) } <-> ( r C_ s /\ ( s o. s ) C_ s ) )
30 eqid 
 |-  NN = NN
31 10 iunrelexpmin1 
 |-  ( ( r e. _V /\ NN = NN ) -> A. s ( ( r C_ s /\ ( s o. s ) C_ s ) -> ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) C_ s ) )
32 30 31 mpan2 
 |-  ( r e. _V -> A. s ( ( r C_ s /\ ( s o. s ) C_ s ) -> ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) C_ s ) )
33 32 19.21bi 
 |-  ( r e. _V -> ( ( r C_ s /\ ( s o. s ) C_ s ) -> ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) C_ s ) )
34 29 33 syl5bi 
 |-  ( r e. _V -> ( s e. { z | ( r C_ z /\ ( z o. z ) C_ z ) } -> ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) C_ s ) )
35 34 ralrimiv 
 |-  ( r e. _V -> A. s e. { z | ( r C_ z /\ ( z o. z ) C_ z ) } ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) C_ s )
36 ssint 
 |-  ( ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) C_ |^| { z | ( r C_ z /\ ( z o. z ) C_ z ) } <-> A. s e. { z | ( r C_ z /\ ( z o. z ) C_ z ) } ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) C_ s )
37 35 36 sylibr 
 |-  ( r e. _V -> ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) C_ |^| { z | ( r C_ z /\ ( z o. z ) C_ z ) } )
38 26 37 eqssd 
 |-  ( r e. _V -> |^| { z | ( r C_ z /\ ( z o. z ) C_ z ) } = ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) )
39 oveq1 
 |-  ( a = r -> ( a ^r n ) = ( r ^r n ) )
40 39 iuneq2d 
 |-  ( a = r -> U_ n e. NN ( a ^r n ) = U_ n e. NN ( r ^r n ) )
41 eqid 
 |-  ( a e. _V |-> U_ n e. NN ( a ^r n ) ) = ( a e. _V |-> U_ n e. NN ( a ^r n ) )
42 ovex 
 |-  ( r ^r n ) e. _V
43 3 42 iunex 
 |-  U_ n e. NN ( r ^r n ) e. _V
44 40 41 43 fvmpt 
 |-  ( r e. _V -> ( ( a e. _V |-> U_ n e. NN ( a ^r n ) ) ` r ) = U_ n e. NN ( r ^r n ) )
45 38 44 eqtrd 
 |-  ( r e. _V -> |^| { z | ( r C_ z /\ ( z o. z ) C_ z ) } = U_ n e. NN ( r ^r n ) )
46 45 mpteq2ia 
 |-  ( r e. _V |-> |^| { z | ( r C_ z /\ ( z o. z ) C_ z ) } ) = ( r e. _V |-> U_ n e. NN ( r ^r n ) )
47 1 46 eqtri 
 |-  t+ = ( r e. _V |-> U_ n e. NN ( r ^r n ) )