Metamath Proof Explorer

Theorem dfrtrcl3

Description: Reflexive-transitive closure of a relation, expressed as indexed union of powers of relations. Generalized from dfrtrcl2 . (Contributed by RP, 5-Jun-2020)

Ref Expression
Assertion dfrtrcl3 
|- t* = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )

Proof

Step Hyp Ref Expression
1 df-rtrcl 
 |-  t* = ( r e. _V |-> |^| { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } )
2 relexp0g 
 |-  ( r e. _V -> ( r ^r 0 ) = ( _I |` ( dom r u. ran r ) ) )
3 nn0ex 
 |-  NN0 e. _V
4 0nn0 
 |-  0 e. NN0
5 oveq1 
 |-  ( a = t -> ( a ^r n ) = ( t ^r n ) )
6 5 iuneq2d 
 |-  ( a = t -> U_ n e. NN0 ( a ^r n ) = U_ n e. NN0 ( t ^r n ) )
7 oveq2 
 |-  ( n = k -> ( t ^r n ) = ( t ^r k ) )
8 7 cbviunv 
 |-  U_ n e. NN0 ( t ^r n ) = U_ k e. NN0 ( t ^r k )
9 6 8 eqtrdi 
 |-  ( a = t -> U_ n e. NN0 ( a ^r n ) = U_ k e. NN0 ( t ^r k ) )
10 9 cbvmptv 
 |-  ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) = ( t e. _V |-> U_ k e. NN0 ( t ^r k ) )
11 10 ov2ssiunov2 
 |-  ( ( r e. _V /\ NN0 e. _V /\ 0 e. NN0 ) -> ( r ^r 0 ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) )
12 3 4 11 mp3an23 
 |-  ( r e. _V -> ( r ^r 0 ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) )
13 2 12 eqsstrrd 
 |-  ( r e. _V -> ( _I |` ( dom r u. ran r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) )
14 relexp1g 
 |-  ( r e. _V -> ( r ^r 1 ) = r )
15 1nn0 
 |-  1 e. NN0
16 10 ov2ssiunov2 
 |-  ( ( r e. _V /\ NN0 e. _V /\ 1 e. NN0 ) -> ( r ^r 1 ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) )
17 3 15 16 mp3an23 
 |-  ( r e. _V -> ( r ^r 1 ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) )
18 14 17 eqsstrrd 
 |-  ( r e. _V -> r C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) )
19 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
20 10 iunrelexpuztr 
 |-  ( ( r e. _V /\ NN0 = ( ZZ>= ` 0 ) /\ 0 e. NN0 ) -> ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) )
21 19 4 20 mp3an23 
 |-  ( r e. _V -> ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) )
22 fvex 
 |-  ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) e. _V
23 sseq2 
 |-  ( z = ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) -> ( ( _I |` ( dom r u. ran r ) ) C_ z <-> ( _I |` ( dom r u. ran r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) )
24 sseq2 
 |-  ( z = ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) -> ( r C_ z <-> r C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) )
25 id 
 |-  ( z = ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) -> z = ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) )
26 25 25 coeq12d 
 |-  ( z = ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) -> ( z o. z ) = ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) )
27 26 25 sseq12d 
 |-  ( z = ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) -> ( ( z o. z ) C_ z <-> ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) )
28 23 24 27 3anbi123d 
 |-  ( z = ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) -> ( ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) <-> ( ( _I |` ( dom r u. ran r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) /\ r C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) /\ ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) ) )
29 28 a1i 
 |-  ( r e. _V -> ( z = ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) -> ( ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) <-> ( ( _I |` ( dom r u. ran r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) /\ r C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) /\ ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) ) ) )
30 29 alrimiv 
 |-  ( r e. _V -> A. z ( z = ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) -> ( ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) <-> ( ( _I |` ( dom r u. ran r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) /\ r C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) /\ ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) ) ) )
31 elabgt 
 |-  ( ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) e. _V /\ A. z ( z = ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) -> ( ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) <-> ( ( _I |` ( dom r u. ran r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) /\ r C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) /\ ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) ) ) ) -> ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) e. { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } <-> ( ( _I |` ( dom r u. ran r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) /\ r C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) /\ ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) ) )
32 22 30 31 sylancr 
 |-  ( r e. _V -> ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) e. { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } <-> ( ( _I |` ( dom r u. ran r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) /\ r C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) /\ ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) o. ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) ) ) )
33 13 18 21 32 mpbir3and 
 |-  ( r e. _V -> ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) e. { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } )
34 intss1 
 |-  ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) e. { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } -> |^| { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) )
35 33 34 syl 
 |-  ( r e. _V -> |^| { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } C_ ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) )
36 vex 
 |-  s e. _V
37 sseq2 
 |-  ( z = s -> ( ( _I |` ( dom r u. ran r ) ) C_ z <-> ( _I |` ( dom r u. ran r ) ) C_ s ) )
38 sseq2 
 |-  ( z = s -> ( r C_ z <-> r C_ s ) )
39 id 
 |-  ( z = s -> z = s )
40 39 39 coeq12d 
 |-  ( z = s -> ( z o. z ) = ( s o. s ) )
41 40 39 sseq12d 
 |-  ( z = s -> ( ( z o. z ) C_ z <-> ( s o. s ) C_ s ) )
42 37 38 41 3anbi123d 
 |-  ( z = s -> ( ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) <-> ( ( _I |` ( dom r u. ran r ) ) C_ s /\ r C_ s /\ ( s o. s ) C_ s ) ) )
43 36 42 elab 
 |-  ( s e. { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } <-> ( ( _I |` ( dom r u. ran r ) ) C_ s /\ r C_ s /\ ( s o. s ) C_ s ) )
44 eqid 
 |-  NN0 = NN0
45 10 iunrelexpmin2 
 |-  ( ( r e. _V /\ NN0 = NN0 ) -> A. s ( ( ( _I |` ( dom r u. ran r ) ) C_ s /\ r C_ s /\ ( s o. s ) C_ s ) -> ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) C_ s ) )
46 44 45 mpan2 
 |-  ( r e. _V -> A. s ( ( ( _I |` ( dom r u. ran r ) ) C_ s /\ r C_ s /\ ( s o. s ) C_ s ) -> ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) C_ s ) )
47 46 19.21bi 
 |-  ( r e. _V -> ( ( ( _I |` ( dom r u. ran r ) ) C_ s /\ r C_ s /\ ( s o. s ) C_ s ) -> ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) C_ s ) )
48 43 47 biimtrid 
 |-  ( r e. _V -> ( s e. { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } -> ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) C_ s ) )
49 48 ralrimiv 
 |-  ( r e. _V -> A. s e. { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) C_ s )
50 ssint 
 |-  ( ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) C_ |^| { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } <-> A. s e. { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) C_ s )
51 49 50 sylibr 
 |-  ( r e. _V -> ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) C_ |^| { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } )
52 35 51 eqssd 
 |-  ( r e. _V -> |^| { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } = ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) )
53 oveq1 
 |-  ( a = r -> ( a ^r n ) = ( r ^r n ) )
54 53 iuneq2d 
 |-  ( a = r -> U_ n e. NN0 ( a ^r n ) = U_ n e. NN0 ( r ^r n ) )
55 eqid 
 |-  ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) = ( a e. _V |-> U_ n e. NN0 ( a ^r n ) )
56 ovex 
 |-  ( r ^r n ) e. _V
57 3 56 iunex 
 |-  U_ n e. NN0 ( r ^r n ) e. _V
58 54 55 57 fvmpt 
 |-  ( r e. _V -> ( ( a e. _V |-> U_ n e. NN0 ( a ^r n ) ) ` r ) = U_ n e. NN0 ( r ^r n ) )
59 52 58 eqtrd 
 |-  ( r e. _V -> |^| { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } = U_ n e. NN0 ( r ^r n ) )
60 59 mpteq2ia 
 |-  ( r e. _V |-> |^| { z | ( ( _I |` ( dom r u. ran r ) ) C_ z /\ r C_ z /\ ( z o. z ) C_ z ) } ) = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )
61 1 60 eqtri 
 |-  t* = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )