Metamath Proof Explorer

Theorem cnvtrcl0

Description: The converse of the transitive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020)

Ref Expression
Assertion cnvtrcl0 
|- ( X e. V -> `' |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } = |^| { y | ( `' X C_ y /\ ( y o. y ) C_ y ) } )

Proof

Step Hyp Ref Expression
1 cnvco 
 |-  `' ( y o. y ) = ( `' y o. `' y )
2 cnvss 
 |-  ( ( y o. y ) C_ y -> `' ( y o. y ) C_ `' y )
3 1 2 eqsstrrid 
 |-  ( ( y o. y ) C_ y -> ( `' y o. `' y ) C_ `' y )
4 coundir 
 |-  ( ( `' y u. ( X \ `' `' X ) ) o. ( `' y u. ( X \ `' `' X ) ) ) = ( ( `' y o. ( `' y u. ( X \ `' `' X ) ) ) u. ( ( X \ `' `' X ) o. ( `' y u. ( X \ `' `' X ) ) ) )
5 coundi 
 |-  ( `' y o. ( `' y u. ( X \ `' `' X ) ) ) = ( ( `' y o. `' y ) u. ( `' y o. ( X \ `' `' X ) ) )
6 ssid 
 |-  ( `' y o. `' y ) C_ ( `' y o. `' y )
7 cononrel2 
 |-  ( `' y o. ( X \ `' `' X ) ) = (/)
8 0ss 
 |-  (/) C_ ( `' y o. `' y )
9 7 8 eqsstri 
 |-  ( `' y o. ( X \ `' `' X ) ) C_ ( `' y o. `' y )
10 6 9 unssi 
 |-  ( ( `' y o. `' y ) u. ( `' y o. ( X \ `' `' X ) ) ) C_ ( `' y o. `' y )
11 5 10 eqsstri 
 |-  ( `' y o. ( `' y u. ( X \ `' `' X ) ) ) C_ ( `' y o. `' y )
12 cononrel1 
 |-  ( ( X \ `' `' X ) o. ( `' y u. ( X \ `' `' X ) ) ) = (/)
13 12 8 eqsstri 
 |-  ( ( X \ `' `' X ) o. ( `' y u. ( X \ `' `' X ) ) ) C_ ( `' y o. `' y )
14 11 13 unssi 
 |-  ( ( `' y o. ( `' y u. ( X \ `' `' X ) ) ) u. ( ( X \ `' `' X ) o. ( `' y u. ( X \ `' `' X ) ) ) ) C_ ( `' y o. `' y )
15 4 14 eqsstri 
 |-  ( ( `' y u. ( X \ `' `' X ) ) o. ( `' y u. ( X \ `' `' X ) ) ) C_ ( `' y o. `' y )
16 id 
 |-  ( ( `' y o. `' y ) C_ `' y -> ( `' y o. `' y ) C_ `' y )
17 15 16 sstrid 
 |-  ( ( `' y o. `' y ) C_ `' y -> ( ( `' y u. ( X \ `' `' X ) ) o. ( `' y u. ( X \ `' `' X ) ) ) C_ `' y )
18 ssun3 
 |-  ( ( ( `' y u. ( X \ `' `' X ) ) o. ( `' y u. ( X \ `' `' X ) ) ) C_ `' y -> ( ( `' y u. ( X \ `' `' X ) ) o. ( `' y u. ( X \ `' `' X ) ) ) C_ ( `' y u. ( X \ `' `' X ) ) )
19 3 17 18 3syl 
 |-  ( ( y o. y ) C_ y -> ( ( `' y u. ( X \ `' `' X ) ) o. ( `' y u. ( X \ `' `' X ) ) ) C_ ( `' y u. ( X \ `' `' X ) ) )
20 id 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> x = ( `' y u. ( X \ `' `' X ) ) )
21 20 20 coeq12d 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> ( x o. x ) = ( ( `' y u. ( X \ `' `' X ) ) o. ( `' y u. ( X \ `' `' X ) ) ) )
22 21 20 sseq12d 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> ( ( x o. x ) C_ x <-> ( ( `' y u. ( X \ `' `' X ) ) o. ( `' y u. ( X \ `' `' X ) ) ) C_ ( `' y u. ( X \ `' `' X ) ) ) )
23 19 22 imbitrrid 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> ( ( y o. y ) C_ y -> ( x o. x ) C_ x ) )
24 23 adantl 
 |-  ( ( X e. V /\ x = ( `' y u. ( X \ `' `' X ) ) ) -> ( ( y o. y ) C_ y -> ( x o. x ) C_ x ) )
25 cnvco 
 |-  `' ( x o. x ) = ( `' x o. `' x )
26 cnvss 
 |-  ( ( x o. x ) C_ x -> `' ( x o. x ) C_ `' x )
27 25 26 eqsstrrid 
 |-  ( ( x o. x ) C_ x -> ( `' x o. `' x ) C_ `' x )
28 id 
 |-  ( y = `' x -> y = `' x )
29 28 28 coeq12d 
 |-  ( y = `' x -> ( y o. y ) = ( `' x o. `' x ) )
30 29 28 sseq12d 
 |-  ( y = `' x -> ( ( y o. y ) C_ y <-> ( `' x o. `' x ) C_ `' x ) )
31 27 30 imbitrrid 
 |-  ( y = `' x -> ( ( x o. x ) C_ x -> ( y o. y ) C_ y ) )
32 31 adantl 
 |-  ( ( X e. V /\ y = `' x ) -> ( ( x o. x ) C_ x -> ( y o. y ) C_ y ) )
33 id 
 |-  ( x = ( X u. ( dom X X. ran X ) ) -> x = ( X u. ( dom X X. ran X ) ) )
34 33 33 coeq12d 
 |-  ( x = ( X u. ( dom X X. ran X ) ) -> ( x o. x ) = ( ( X u. ( dom X X. ran X ) ) o. ( X u. ( dom X X. ran X ) ) ) )
35 34 33 sseq12d 
 |-  ( x = ( X u. ( dom X X. ran X ) ) -> ( ( x o. x ) C_ x <-> ( ( X u. ( dom X X. ran X ) ) o. ( X u. ( dom X X. ran X ) ) ) C_ ( X u. ( dom X X. ran X ) ) ) )
36 ssun1 
 |-  X C_ ( X u. ( dom X X. ran X ) )
37 36 a1i 
 |-  ( X e. V -> X C_ ( X u. ( dom X X. ran X ) ) )
38 trclexlem 
 |-  ( X e. V -> ( X u. ( dom X X. ran X ) ) e. _V )
39 coundir 
 |-  ( ( X u. ( dom X X. ran X ) ) o. ( X u. ( dom X X. ran X ) ) ) = ( ( X o. ( X u. ( dom X X. ran X ) ) ) u. ( ( dom X X. ran X ) o. ( X u. ( dom X X. ran X ) ) ) )
40 coundi 
 |-  ( X o. ( X u. ( dom X X. ran X ) ) ) = ( ( X o. X ) u. ( X o. ( dom X X. ran X ) ) )
41 cossxp 
 |-  ( X o. X ) C_ ( dom X X. ran X )
42 cossxp 
 |-  ( X o. ( dom X X. ran X ) ) C_ ( dom ( dom X X. ran X ) X. ran X )
43 dmxpss 
 |-  dom ( dom X X. ran X ) C_ dom X
44 xpss1 
 |-  ( dom ( dom X X. ran X ) C_ dom X -> ( dom ( dom X X. ran X ) X. ran X ) C_ ( dom X X. ran X ) )
45 43 44 ax-mp 
 |-  ( dom ( dom X X. ran X ) X. ran X ) C_ ( dom X X. ran X )
46 42 45 sstri 
 |-  ( X o. ( dom X X. ran X ) ) C_ ( dom X X. ran X )
47 41 46 unssi 
 |-  ( ( X o. X ) u. ( X o. ( dom X X. ran X ) ) ) C_ ( dom X X. ran X )
48 40 47 eqsstri 
 |-  ( X o. ( X u. ( dom X X. ran X ) ) ) C_ ( dom X X. ran X )
49 coundi 
 |-  ( ( dom X X. ran X ) o. ( X u. ( dom X X. ran X ) ) ) = ( ( ( dom X X. ran X ) o. X ) u. ( ( dom X X. ran X ) o. ( dom X X. ran X ) ) )
50 cossxp 
 |-  ( ( dom X X. ran X ) o. X ) C_ ( dom X X. ran ( dom X X. ran X ) )
51 rnxpss 
 |-  ran ( dom X X. ran X ) C_ ran X
52 xpss2 
 |-  ( ran ( dom X X. ran X ) C_ ran X -> ( dom X X. ran ( dom X X. ran X ) ) C_ ( dom X X. ran X ) )
53 51 52 ax-mp 
 |-  ( dom X X. ran ( dom X X. ran X ) ) C_ ( dom X X. ran X )
54 50 53 sstri 
 |-  ( ( dom X X. ran X ) o. X ) C_ ( dom X X. ran X )
55 xptrrel 
 |-  ( ( dom X X. ran X ) o. ( dom X X. ran X ) ) C_ ( dom X X. ran X )
56 54 55 unssi 
 |-  ( ( ( dom X X. ran X ) o. X ) u. ( ( dom X X. ran X ) o. ( dom X X. ran X ) ) ) C_ ( dom X X. ran X )
57 49 56 eqsstri 
 |-  ( ( dom X X. ran X ) o. ( X u. ( dom X X. ran X ) ) ) C_ ( dom X X. ran X )
58 48 57 unssi 
 |-  ( ( X o. ( X u. ( dom X X. ran X ) ) ) u. ( ( dom X X. ran X ) o. ( X u. ( dom X X. ran X ) ) ) ) C_ ( dom X X. ran X )
59 39 58 eqsstri 
 |-  ( ( X u. ( dom X X. ran X ) ) o. ( X u. ( dom X X. ran X ) ) ) C_ ( dom X X. ran X )
60 ssun2 
 |-  ( dom X X. ran X ) C_ ( X u. ( dom X X. ran X ) )
61 59 60 sstri 
 |-  ( ( X u. ( dom X X. ran X ) ) o. ( X u. ( dom X X. ran X ) ) ) C_ ( X u. ( dom X X. ran X ) )
62 61 a1i 
 |-  ( X e. V -> ( ( X u. ( dom X X. ran X ) ) o. ( X u. ( dom X X. ran X ) ) ) C_ ( X u. ( dom X X. ran X ) ) )
63 24 32 35 37 38 62 clcnvlem 
 |-  ( X e. V -> `' |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } = |^| { y | ( `' X C_ y /\ ( y o. y ) C_ y ) } )