Metamath Proof Explorer

Theorem dfrtrcl5

Description: Definition of reflexive-transitive closure as a standard closure. (Contributed by RP, 1-Nov-2020)

Ref Expression
Assertion dfrtrcl5 
|- t* = ( x e. _V |-> |^| { y | ( x C_ y /\ ( ( _I |` ( dom y u. ran y ) ) C_ y /\ ( y o. y ) C_ y ) ) } )

Proof

Step Hyp Ref Expression
1 df-rtrcl 
 |-  t* = ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } )
2 ancom 
 |-  ( ( ( _I |` ( dom y u. ran y ) ) C_ y /\ ( y o. y ) C_ y ) <-> ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) )
3 2 anbi2i 
 |-  ( ( x C_ y /\ ( ( _I |` ( dom y u. ran y ) ) C_ y /\ ( y o. y ) C_ y ) ) <-> ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) )
4 3 abbii 
 |-  { y | ( x C_ y /\ ( ( _I |` ( dom y u. ran y ) ) C_ y /\ ( y o. y ) C_ y ) ) } = { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) }
5 4 inteqi 
 |-  |^| { y | ( x C_ y /\ ( ( _I |` ( dom y u. ran y ) ) C_ y /\ ( y o. y ) C_ y ) ) } = |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) }
6 5 mpteq2i 
 |-  ( x e. _V |-> |^| { y | ( x C_ y /\ ( ( _I |` ( dom y u. ran y ) ) C_ y /\ ( y o. y ) C_ y ) ) } ) = ( x e. _V |-> |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } )
7 vex 
 |-  x e. _V
8 7 rtrclexi 
 |-  |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } e. _V
9 8 a1i 
 |-  ( x e. _V -> |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } e. _V )
10 dmexg 
 |-  ( x e. _V -> dom x e. _V )
11 rnexg 
 |-  ( x e. _V -> ran x e. _V )
12 unexg 
 |-  ( ( dom x e. _V /\ ran x e. _V ) -> ( dom x u. ran x ) e. _V )
13 10 11 12 syl2anc 
 |-  ( x e. _V -> ( dom x u. ran x ) e. _V )
14 resiexg 
 |-  ( ( dom x u. ran x ) e. _V -> ( _I |` ( dom x u. ran x ) ) e. _V )
15 7 13 14 mp2b 
 |-  ( _I |` ( dom x u. ran x ) ) e. _V
16 7 15 unex 
 |-  ( x u. ( _I |` ( dom x u. ran x ) ) ) e. _V
17 16 trclexi 
 |-  |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } e. _V
18 17 a1i 
 |-  ( x e. _V -> |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } e. _V )
19 simpr 
 |-  ( ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) -> ( z o. z ) C_ z )
20 19 cotrintab 
 |-  ( |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } o. |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) C_ |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) }
21 20 a1i 
 |-  ( x e. _V -> ( |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } o. |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) C_ |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } )
22 7 dmex 
 |-  dom x e. _V
23 7 rnex 
 |-  ran x e. _V
24 12 resiexd 
 |-  ( ( dom x e. _V /\ ran x e. _V ) -> ( _I |` ( dom x u. ran x ) ) e. _V )
25 22 23 24 mp2an 
 |-  ( _I |` ( dom x u. ran x ) ) e. _V
26 7 25 unex 
 |-  ( x u. ( _I |` ( dom x u. ran x ) ) ) e. _V
27 dmtrcl 
 |-  ( ( x u. ( _I |` ( dom x u. ran x ) ) ) e. _V -> dom |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } = dom ( x u. ( _I |` ( dom x u. ran x ) ) ) )
28 26 27 ax-mp 
 |-  dom |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } = dom ( x u. ( _I |` ( dom x u. ran x ) ) )
29 dmun 
 |-  dom ( x u. ( _I |` ( dom x u. ran x ) ) ) = ( dom x u. dom ( _I |` ( dom x u. ran x ) ) )
30 dmresi 
 |-  dom ( _I |` ( dom x u. ran x ) ) = ( dom x u. ran x )
31 30 uneq2i 
 |-  ( dom x u. dom ( _I |` ( dom x u. ran x ) ) ) = ( dom x u. ( dom x u. ran x ) )
32 ssun1 
 |-  dom x C_ ( dom x u. ran x )
33 ssequn1 
 |-  ( dom x C_ ( dom x u. ran x ) <-> ( dom x u. ( dom x u. ran x ) ) = ( dom x u. ran x ) )
34 32 33 mpbi 
 |-  ( dom x u. ( dom x u. ran x ) ) = ( dom x u. ran x )
35 29 31 34 3eqtri 
 |-  dom ( x u. ( _I |` ( dom x u. ran x ) ) ) = ( dom x u. ran x )
36 28 35 eqtri 
 |-  dom |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } = ( dom x u. ran x )
37 rntrcl 
 |-  ( ( x u. ( _I |` ( dom x u. ran x ) ) ) e. _V -> ran |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } = ran ( x u. ( _I |` ( dom x u. ran x ) ) ) )
38 26 37 ax-mp 
 |-  ran |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } = ran ( x u. ( _I |` ( dom x u. ran x ) ) )
39 rnun 
 |-  ran ( x u. ( _I |` ( dom x u. ran x ) ) ) = ( ran x u. ran ( _I |` ( dom x u. ran x ) ) )
40 rnresi 
 |-  ran ( _I |` ( dom x u. ran x ) ) = ( dom x u. ran x )
41 40 uneq2i 
 |-  ( ran x u. ran ( _I |` ( dom x u. ran x ) ) ) = ( ran x u. ( dom x u. ran x ) )
42 ssun2 
 |-  ran x C_ ( dom x u. ran x )
43 ssequn1 
 |-  ( ran x C_ ( dom x u. ran x ) <-> ( ran x u. ( dom x u. ran x ) ) = ( dom x u. ran x ) )
44 42 43 mpbi 
 |-  ( ran x u. ( dom x u. ran x ) ) = ( dom x u. ran x )
45 39 41 44 3eqtri 
 |-  ran ( x u. ( _I |` ( dom x u. ran x ) ) ) = ( dom x u. ran x )
46 38 45 eqtri 
 |-  ran |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } = ( dom x u. ran x )
47 36 46 uneq12i 
 |-  ( dom |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } u. ran |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) = ( ( dom x u. ran x ) u. ( dom x u. ran x ) )
48 unidm 
 |-  ( ( dom x u. ran x ) u. ( dom x u. ran x ) ) = ( dom x u. ran x )
49 47 48 eqtri 
 |-  ( dom |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } u. ran |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) = ( dom x u. ran x )
50 49 reseq2i 
 |-  ( _I |` ( dom |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } u. ran |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) ) = ( _I |` ( dom x u. ran x ) )
51 ssun2 
 |-  ( _I |` ( dom x u. ran x ) ) C_ ( x u. ( _I |` ( dom x u. ran x ) ) )
52 ssmin 
 |-  ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) }
53 51 52 sstri 
 |-  ( _I |` ( dom x u. ran x ) ) C_ |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) }
54 50 53 eqsstri 
 |-  ( _I |` ( dom |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } u. ran |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) ) C_ |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) }
55 54 a1i 
 |-  ( x e. _V -> ( _I |` ( dom |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } u. ran |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) ) C_ |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } )
56 simprl 
 |-  ( ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) -> ( y o. y ) C_ y )
57 56 cotrintab 
 |-  ( |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } o. |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } ) C_ |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) }
58 57 a1i 
 |-  ( x e. _V -> ( |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } o. |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } ) C_ |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } )
59 id 
 |-  ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } -> y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } )
60 59 59 coeq12d 
 |-  ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } -> ( y o. y ) = ( |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } o. |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) )
61 60 59 sseq12d 
 |-  ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } -> ( ( y o. y ) C_ y <-> ( |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } o. |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) C_ |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) )
62 dmeq 
 |-  ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } -> dom y = dom |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } )
63 rneq 
 |-  ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } -> ran y = ran |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } )
64 62 63 uneq12d 
 |-  ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } -> ( dom y u. ran y ) = ( dom |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } u. ran |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) )
65 64 reseq2d 
 |-  ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } -> ( _I |` ( dom y u. ran y ) ) = ( _I |` ( dom |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } u. ran |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) ) )
66 65 59 sseq12d 
 |-  ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } -> ( ( _I |` ( dom y u. ran y ) ) C_ y <-> ( _I |` ( dom |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } u. ran |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) ) C_ |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) )
67 id 
 |-  ( z = |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } -> z = |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } )
68 67 67 coeq12d 
 |-  ( z = |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } -> ( z o. z ) = ( |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } o. |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } ) )
69 68 67 sseq12d 
 |-  ( z = |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } -> ( ( z o. z ) C_ z <-> ( |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } o. |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } ) C_ |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } ) )
70 9 18 21 55 58 61 66 69 mptrcllem 
 |-  ( x e. _V |-> |^| { y | ( x C_ y /\ ( ( y o. y ) C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } ) = ( x e. _V |-> |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } )
71 df-3an 
 |-  ( ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) <-> ( ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z ) /\ ( z o. z ) C_ z ) )
72 ancom 
 |-  ( ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z ) <-> ( x C_ z /\ ( _I |` ( dom x u. ran x ) ) C_ z ) )
73 unss 
 |-  ( ( x C_ z /\ ( _I |` ( dom x u. ran x ) ) C_ z ) <-> ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z )
74 72 73 bitri 
 |-  ( ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z ) <-> ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z )
75 74 anbi1i 
 |-  ( ( ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z ) /\ ( z o. z ) C_ z ) <-> ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) )
76 71 75 bitr2i 
 |-  ( ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) <-> ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) )
77 76 abbii 
 |-  { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } = { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) }
78 77 inteqi 
 |-  |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } = |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) }
79 78 mpteq2i 
 |-  ( x e. _V |-> |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ( z o. z ) C_ z ) } ) = ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } )
80 6 70 79 3eqtri 
 |-  ( x e. _V |-> |^| { y | ( x C_ y /\ ( ( _I |` ( dom y u. ran y ) ) C_ y /\ ( y o. y ) C_ y ) ) } ) = ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } )
81 1 80 eqtr4i 
 |-  t* = ( x e. _V |-> |^| { y | ( x C_ y /\ ( ( _I |` ( dom y u. ran y ) ) C_ y /\ ( y o. y ) C_ y ) ) } )