Metamath Proof Explorer

Theorem dfrtrcl2

Description: The two definitions t* and t*rec of the reflexive, transitive closure coincide if R is indeed a relation. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 13-Jul-2024)

Ref Expression
Hypothesis dfrtrcl2.1 
|- ( ph -> Rel R )
Assertion dfrtrcl2 
|- ( ph -> ( t* ` R ) = ( t*rec ` R ) )

Proof

Step Hyp Ref Expression
1 dfrtrcl2.1 
 |-  ( ph -> Rel R )
2 eqidd 
 |-  ( ( ph /\ R e. _V ) -> ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ 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 ) } ) )
3 dmeq 
 |-  ( x = R -> dom x = dom R )
4 rneq 
 |-  ( x = R -> ran x = ran R )
5 3 4 uneq12d 
 |-  ( x = R -> ( dom x u. ran x ) = ( dom R u. ran R ) )
6 5 reseq2d 
 |-  ( x = R -> ( _I |` ( dom x u. ran x ) ) = ( _I |` ( dom R u. ran R ) ) )
7 6 sseq1d 
 |-  ( x = R -> ( ( _I |` ( dom x u. ran x ) ) C_ z <-> ( _I |` ( dom R u. ran R ) ) C_ z ) )
8 id 
 |-  ( x = R -> x = R )
9 8 sseq1d 
 |-  ( x = R -> ( x C_ z <-> R C_ z ) )
10 7 9 3anbi12d 
 |-  ( x = R -> ( ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) <-> ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) ) )
11 10 abbidv 
 |-  ( x = R -> { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } = { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } )
12 11 inteqd 
 |-  ( x = R -> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } = |^| { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } )
13 12 adantl 
 |-  ( ( ( ph /\ R e. _V ) /\ x = R ) -> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } = |^| { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } )
14 simpr 
 |-  ( ( ph /\ R e. _V ) -> R e. _V )
15 relfld 
 |-  ( Rel R -> U. U. R = ( dom R u. ran R ) )
16 1 15 syl 
 |-  ( ph -> U. U. R = ( dom R u. ran R ) )
17 16 eqcomd 
 |-  ( ph -> ( dom R u. ran R ) = U. U. R )
18 17 adantr 
 |-  ( ( ph /\ R e. _V ) -> ( dom R u. ran R ) = U. U. R )
19 1 adantr 
 |-  ( ( ph /\ R e. _V ) -> Rel R )
20 19 14 rtrclreclem2 
 |-  ( ( ph /\ R e. _V ) -> ( _I |` U. U. R ) C_ ( t*rec ` R ) )
21 id 
 |-  ( ( dom R u. ran R ) = U. U. R -> ( dom R u. ran R ) = U. U. R )
22 21 reseq2d 
 |-  ( ( dom R u. ran R ) = U. U. R -> ( _I |` ( dom R u. ran R ) ) = ( _I |` U. U. R ) )
23 22 sseq1d 
 |-  ( ( dom R u. ran R ) = U. U. R -> ( ( _I |` ( dom R u. ran R ) ) C_ ( t*rec ` R ) <-> ( _I |` U. U. R ) C_ ( t*rec ` R ) ) )
24 20 23 imbitrrid 
 |-  ( ( dom R u. ran R ) = U. U. R -> ( ( ph /\ R e. _V ) -> ( _I |` ( dom R u. ran R ) ) C_ ( t*rec ` R ) ) )
25 18 24 mpcom 
 |-  ( ( ph /\ R e. _V ) -> ( _I |` ( dom R u. ran R ) ) C_ ( t*rec ` R ) )
26 14 rtrclreclem1 
 |-  ( ( ph /\ R e. _V ) -> R C_ ( t*rec ` R ) )
27 1 rtrclreclem3 
 |-  ( ph -> ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) )
28 27 adantr 
 |-  ( ( ph /\ R e. _V ) -> ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) )
29 fvex 
 |-  ( t*rec ` R ) e. _V
30 sseq2 
 |-  ( z = ( t*rec ` R ) -> ( ( _I |` ( dom R u. ran R ) ) C_ z <-> ( _I |` ( dom R u. ran R ) ) C_ ( t*rec ` R ) ) )
31 sseq2 
 |-  ( z = ( t*rec ` R ) -> ( R C_ z <-> R C_ ( t*rec ` R ) ) )
32 id 
 |-  ( z = ( t*rec ` R ) -> z = ( t*rec ` R ) )
33 32 32 coeq12d 
 |-  ( z = ( t*rec ` R ) -> ( z o. z ) = ( ( t*rec ` R ) o. ( t*rec ` R ) ) )
34 33 32 sseq12d 
 |-  ( z = ( t*rec ` R ) -> ( ( z o. z ) C_ z <-> ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) ) )
35 30 31 34 3anbi123d 
 |-  ( z = ( t*rec ` R ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) <-> ( ( _I |` ( dom R u. ran R ) ) C_ ( t*rec ` R ) /\ R C_ ( t*rec ` R ) /\ ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) ) ) )
36 35 a1i 
 |-  ( ph -> ( z = ( t*rec ` R ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) <-> ( ( _I |` ( dom R u. ran R ) ) C_ ( t*rec ` R ) /\ R C_ ( t*rec ` R ) /\ ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) ) ) ) )
37 36 alrimiv 
 |-  ( ph -> A. z ( z = ( t*rec ` R ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) <-> ( ( _I |` ( dom R u. ran R ) ) C_ ( t*rec ` R ) /\ R C_ ( t*rec ` R ) /\ ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) ) ) ) )
38 elabgt 
 |-  ( ( ( t*rec ` R ) e. _V /\ A. z ( z = ( t*rec ` R ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) <-> ( ( _I |` ( dom R u. ran R ) ) C_ ( t*rec ` R ) /\ R C_ ( t*rec ` R ) /\ ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) ) ) ) ) -> ( ( t*rec ` 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_ ( t*rec ` R ) /\ R C_ ( t*rec ` R ) /\ ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) ) ) )
39 29 37 38 sylancr 
 |-  ( ph -> ( ( t*rec ` 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_ ( t*rec ` R ) /\ R C_ ( t*rec ` R ) /\ ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) ) ) )
40 39 adantr 
 |-  ( ( ph /\ R e. _V ) -> ( ( t*rec ` 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_ ( t*rec ` R ) /\ R C_ ( t*rec ` R ) /\ ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) ) ) )
41 25 26 28 40 mpbir3and 
 |-  ( ( ph /\ R e. _V ) -> ( t*rec ` R ) e. { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } )
42 41 ne0d 
 |-  ( ( ph /\ R e. _V ) -> { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } =/= (/) )
43 intex 
 |-  ( { 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 ) } e. _V )
44 42 43 sylib 
 |-  ( ( ph /\ R e. _V ) -> |^| { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } e. _V )
45 2 13 14 44 fvmptd 
 |-  ( ( ph /\ R e. _V ) -> ( ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } ) ` R ) = |^| { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } )
46 intss1 
 |-  ( ( t*rec ` 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_ ( t*rec ` R ) )
47 41 46 syl 
 |-  ( ( ph /\ R e. _V ) -> |^| { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } C_ ( t*rec ` R ) )
48 vex 
 |-  s e. _V
49 sseq2 
 |-  ( z = s -> ( ( _I |` ( dom R u. ran R ) ) C_ z <-> ( _I |` ( dom R u. ran R ) ) C_ s ) )
50 sseq2 
 |-  ( z = s -> ( R C_ z <-> R C_ s ) )
51 id 
 |-  ( z = s -> z = s )
52 51 51 coeq12d 
 |-  ( z = s -> ( z o. z ) = ( s o. s ) )
53 52 51 sseq12d 
 |-  ( z = s -> ( ( z o. z ) C_ z <-> ( s o. s ) C_ s ) )
54 49 50 53 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 ) ) )
55 48 54 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 ) )
56 1 rtrclreclem4 
 |-  ( ph -> A. s ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( t*rec ` R ) C_ s ) )
57 56 19.21bi 
 |-  ( ph -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( t*rec ` R ) C_ s ) )
58 55 57 biimtrid 
 |-  ( ph -> ( s e. { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } -> ( t*rec ` R ) C_ s ) )
59 58 ralrimiv 
 |-  ( ph -> A. s e. { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } ( t*rec ` R ) C_ s )
60 ssint 
 |-  ( ( t*rec ` 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 ) } ( t*rec ` R ) C_ s )
61 59 60 sylibr 
 |-  ( ph -> ( t*rec ` R ) C_ |^| { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } )
62 61 adantr 
 |-  ( ( ph /\ R e. _V ) -> ( t*rec ` R ) C_ |^| { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } )
63 47 62 eqssd 
 |-  ( ( ph /\ R e. _V ) -> |^| { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } = ( t*rec ` R ) )
64 45 63 eqtrd 
 |-  ( ( ph /\ R e. _V ) -> ( ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } ) ` R ) = ( t*rec ` R ) )
65 df-rtrcl 
 |-  t* = ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } )
66 fveq1 
 |-  ( t* = ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } ) -> ( t* ` R ) = ( ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } ) ` R ) )
67 66 eqeq1d 
 |-  ( t* = ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } ) -> ( ( t* ` R ) = ( t*rec ` R ) <-> ( ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } ) ` R ) = ( t*rec ` R ) ) )
68 67 imbi2d 
 |-  ( t* = ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } ) -> ( ( ( ph /\ R e. _V ) -> ( t* ` R ) = ( t*rec ` R ) ) <-> ( ( ph /\ R e. _V ) -> ( ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } ) ` R ) = ( t*rec ` R ) ) ) )
69 65 68 ax-mp 
 |-  ( ( ( ph /\ R e. _V ) -> ( t* ` R ) = ( t*rec ` R ) ) <-> ( ( ph /\ R e. _V ) -> ( ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } ) ` R ) = ( t*rec ` R ) ) )
70 64 69 mpbir 
 |-  ( ( ph /\ R e. _V ) -> ( t* ` R ) = ( t*rec ` R ) )
71 70 ex 
 |-  ( ph -> ( R e. _V -> ( t* ` R ) = ( t*rec ` R ) ) )
72 fvprc 
 |-  ( -. R e. _V -> ( t* ` R ) = (/) )
73 fvprc 
 |-  ( -. R e. _V -> ( t*rec ` R ) = (/) )
74 73 eqcomd 
 |-  ( -. R e. _V -> (/) = ( t*rec ` R ) )
75 72 74 eqtrd 
 |-  ( -. R e. _V -> ( t* ` R ) = ( t*rec ` R ) )
76 71 75 pm2.61d1 
 |-  ( ph -> ( t* ` R ) = ( t*rec ` R ) )