Metamath Proof Explorer

Theorem cnvrcl0

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

Ref Expression
Assertion cnvrcl0 
|- ( X e. V -> `' |^| { x | ( X C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) } = |^| { y | ( `' X C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) } )

Proof

Step Hyp Ref Expression
1 cnvresid 
 |-  `' ( _I |` ( dom y u. ran y ) ) = ( _I |` ( dom y u. ran y ) )
2 cnvnonrel 
 |-  `' ( X \ `' `' X ) = (/)
3 cnv0 
 |-  `' (/) = (/)
4 2 3 eqtr4i 
 |-  `' ( X \ `' `' X ) = `' (/)
5 4 dmeqi 
 |-  dom `' ( X \ `' `' X ) = dom `' (/)
6 df-rn 
 |-  ran ( X \ `' `' X ) = dom `' ( X \ `' `' X )
7 df-rn 
 |-  ran (/) = dom `' (/)
8 5 6 7 3eqtr4i 
 |-  ran ( X \ `' `' X ) = ran (/)
9 0ss 
 |-  (/) C_ `' y
10 9 rnssi 
 |-  ran (/) C_ ran `' y
11 8 10 eqsstri 
 |-  ran ( X \ `' `' X ) C_ ran `' y
12 ssequn2 
 |-  ( ran ( X \ `' `' X ) C_ ran `' y <-> ( ran `' y u. ran ( X \ `' `' X ) ) = ran `' y )
13 11 12 mpbi 
 |-  ( ran `' y u. ran ( X \ `' `' X ) ) = ran `' y
14 rnun 
 |-  ran ( `' y u. ( X \ `' `' X ) ) = ( ran `' y u. ran ( X \ `' `' X ) )
15 dfdm4 
 |-  dom y = ran `' y
16 13 14 15 3eqtr4ri 
 |-  dom y = ran ( `' y u. ( X \ `' `' X ) )
17 4 rneqi 
 |-  ran `' ( X \ `' `' X ) = ran `' (/)
18 dfdm4 
 |-  dom ( X \ `' `' X ) = ran `' ( X \ `' `' X )
19 dfdm4 
 |-  dom (/) = ran `' (/)
20 17 18 19 3eqtr4i 
 |-  dom ( X \ `' `' X ) = dom (/)
21 dmss 
 |-  ( (/) C_ `' y -> dom (/) C_ dom `' y )
22 9 21 ax-mp 
 |-  dom (/) C_ dom `' y
23 20 22 eqsstri 
 |-  dom ( X \ `' `' X ) C_ dom `' y
24 ssequn2 
 |-  ( dom ( X \ `' `' X ) C_ dom `' y <-> ( dom `' y u. dom ( X \ `' `' X ) ) = dom `' y )
25 23 24 mpbi 
 |-  ( dom `' y u. dom ( X \ `' `' X ) ) = dom `' y
26 dmun 
 |-  dom ( `' y u. ( X \ `' `' X ) ) = ( dom `' y u. dom ( X \ `' `' X ) )
27 df-rn 
 |-  ran y = dom `' y
28 25 26 27 3eqtr4ri 
 |-  ran y = dom ( `' y u. ( X \ `' `' X ) )
29 16 28 uneq12i 
 |-  ( dom y u. ran y ) = ( ran ( `' y u. ( X \ `' `' X ) ) u. dom ( `' y u. ( X \ `' `' X ) ) )
30 29 equncomi 
 |-  ( dom y u. ran y ) = ( dom ( `' y u. ( X \ `' `' X ) ) u. ran ( `' y u. ( X \ `' `' X ) ) )
31 30 reseq2i 
 |-  ( _I |` ( dom y u. ran y ) ) = ( _I |` ( dom ( `' y u. ( X \ `' `' X ) ) u. ran ( `' y u. ( X \ `' `' X ) ) ) )
32 1 31 eqtr2i 
 |-  ( _I |` ( dom ( `' y u. ( X \ `' `' X ) ) u. ran ( `' y u. ( X \ `' `' X ) ) ) ) = `' ( _I |` ( dom y u. ran y ) )
33 cnvss 
 |-  ( ( _I |` ( dom y u. ran y ) ) C_ y -> `' ( _I |` ( dom y u. ran y ) ) C_ `' y )
34 32 33 eqsstrid 
 |-  ( ( _I |` ( dom y u. ran y ) ) C_ y -> ( _I |` ( dom ( `' y u. ( X \ `' `' X ) ) u. ran ( `' y u. ( X \ `' `' X ) ) ) ) C_ `' y )
35 ssun1 
 |-  `' y C_ ( `' y u. ( X \ `' `' X ) )
36 34 35 sstrdi 
 |-  ( ( _I |` ( dom y u. ran y ) ) C_ y -> ( _I |` ( dom ( `' y u. ( X \ `' `' X ) ) u. ran ( `' y u. ( X \ `' `' X ) ) ) ) C_ ( `' y u. ( X \ `' `' X ) ) )
37 dmeq 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> dom x = dom ( `' y u. ( X \ `' `' X ) ) )
38 rneq 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> ran x = ran ( `' y u. ( X \ `' `' X ) ) )
39 37 38 uneq12d 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> ( dom x u. ran x ) = ( dom ( `' y u. ( X \ `' `' X ) ) u. ran ( `' y u. ( X \ `' `' X ) ) ) )
40 39 reseq2d 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> ( _I |` ( dom x u. ran x ) ) = ( _I |` ( dom ( `' y u. ( X \ `' `' X ) ) u. ran ( `' y u. ( X \ `' `' X ) ) ) ) )
41 id 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> x = ( `' y u. ( X \ `' `' X ) ) )
42 40 41 sseq12d 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> ( ( _I |` ( dom x u. ran x ) ) C_ x <-> ( _I |` ( dom ( `' y u. ( X \ `' `' X ) ) u. ran ( `' y u. ( X \ `' `' X ) ) ) ) C_ ( `' y u. ( X \ `' `' X ) ) ) )
43 36 42 syl5ibr 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> ( ( _I |` ( dom y u. ran y ) ) C_ y -> ( _I |` ( dom x u. ran x ) ) C_ x ) )
44 43 adantl 
 |-  ( ( X e. V /\ x = ( `' y u. ( X \ `' `' X ) ) ) -> ( ( _I |` ( dom y u. ran y ) ) C_ y -> ( _I |` ( dom x u. ran x ) ) C_ x ) )
45 cnvresid 
 |-  `' ( _I |` ( dom x u. ran x ) ) = ( _I |` ( dom x u. ran x ) )
46 dfdm4 
 |-  dom x = ran `' x
47 df-rn 
 |-  ran x = dom `' x
48 46 47 uneq12i 
 |-  ( dom x u. ran x ) = ( ran `' x u. dom `' x )
49 48 equncomi 
 |-  ( dom x u. ran x ) = ( dom `' x u. ran `' x )
50 49 reseq2i 
 |-  ( _I |` ( dom x u. ran x ) ) = ( _I |` ( dom `' x u. ran `' x ) )
51 45 50 eqtr2i 
 |-  ( _I |` ( dom `' x u. ran `' x ) ) = `' ( _I |` ( dom x u. ran x ) )
52 cnvss 
 |-  ( ( _I |` ( dom x u. ran x ) ) C_ x -> `' ( _I |` ( dom x u. ran x ) ) C_ `' x )
53 51 52 eqsstrid 
 |-  ( ( _I |` ( dom x u. ran x ) ) C_ x -> ( _I |` ( dom `' x u. ran `' x ) ) C_ `' x )
54 dmeq 
 |-  ( y = `' x -> dom y = dom `' x )
55 rneq 
 |-  ( y = `' x -> ran y = ran `' x )
56 54 55 uneq12d 
 |-  ( y = `' x -> ( dom y u. ran y ) = ( dom `' x u. ran `' x ) )
57 56 reseq2d 
 |-  ( y = `' x -> ( _I |` ( dom y u. ran y ) ) = ( _I |` ( dom `' x u. ran `' x ) ) )
58 id 
 |-  ( y = `' x -> y = `' x )
59 57 58 sseq12d 
 |-  ( y = `' x -> ( ( _I |` ( dom y u. ran y ) ) C_ y <-> ( _I |` ( dom `' x u. ran `' x ) ) C_ `' x ) )
60 53 59 syl5ibr 
 |-  ( y = `' x -> ( ( _I |` ( dom x u. ran x ) ) C_ x -> ( _I |` ( dom y u. ran y ) ) C_ y ) )
61 60 adantl 
 |-  ( ( X e. V /\ y = `' x ) -> ( ( _I |` ( dom x u. ran x ) ) C_ x -> ( _I |` ( dom y u. ran y ) ) C_ y ) )
62 dmeq 
 |-  ( x = ( X u. ( _I |` ( dom X u. ran X ) ) ) -> dom x = dom ( X u. ( _I |` ( dom X u. ran X ) ) ) )
63 rneq 
 |-  ( x = ( X u. ( _I |` ( dom X u. ran X ) ) ) -> ran x = ran ( X u. ( _I |` ( dom X u. ran X ) ) ) )
64 62 63 uneq12d 
 |-  ( x = ( X u. ( _I |` ( dom X u. ran X ) ) ) -> ( dom x u. ran x ) = ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) u. ran ( X u. ( _I |` ( dom X u. ran X ) ) ) ) )
65 64 reseq2d 
 |-  ( x = ( X u. ( _I |` ( dom X u. ran X ) ) ) -> ( _I |` ( dom x u. ran x ) ) = ( _I |` ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) u. ran ( X u. ( _I |` ( dom X u. ran X ) ) ) ) ) )
66 id 
 |-  ( x = ( X u. ( _I |` ( dom X u. ran X ) ) ) -> x = ( X u. ( _I |` ( dom X u. ran X ) ) ) )
67 65 66 sseq12d 
 |-  ( x = ( X u. ( _I |` ( dom X u. ran X ) ) ) -> ( ( _I |` ( dom x u. ran x ) ) C_ x <-> ( _I |` ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) u. ran ( X u. ( _I |` ( dom X u. ran X ) ) ) ) ) C_ ( X u. ( _I |` ( dom X u. ran X ) ) ) ) )
68 ssun1 
 |-  X C_ ( X u. ( _I |` ( dom X u. ran X ) ) )
69 68 a1i 
 |-  ( X e. V -> X C_ ( X u. ( _I |` ( dom X u. ran X ) ) ) )
70 dmexg 
 |-  ( X e. V -> dom X e. _V )
71 rnexg 
 |-  ( X e. V -> ran X e. _V )
72 unexg 
 |-  ( ( dom X e. _V /\ ran X e. _V ) -> ( dom X u. ran X ) e. _V )
73 70 71 72 syl2anc 
 |-  ( X e. V -> ( dom X u. ran X ) e. _V )
74 73 resiexd 
 |-  ( X e. V -> ( _I |` ( dom X u. ran X ) ) e. _V )
75 unexg 
 |-  ( ( X e. V /\ ( _I |` ( dom X u. ran X ) ) e. _V ) -> ( X u. ( _I |` ( dom X u. ran X ) ) ) e. _V )
76 74 75 mpdan 
 |-  ( X e. V -> ( X u. ( _I |` ( dom X u. ran X ) ) ) e. _V )
77 dmun 
 |-  dom ( X u. ( _I |` ( dom X u. ran X ) ) ) = ( dom X u. dom ( _I |` ( dom X u. ran X ) ) )
78 ssun1 
 |-  dom X C_ ( dom X u. ran X )
79 dmresi 
 |-  dom ( _I |` ( dom X u. ran X ) ) = ( dom X u. ran X )
80 79 eqimssi 
 |-  dom ( _I |` ( dom X u. ran X ) ) C_ ( dom X u. ran X )
81 78 80 unssi 
 |-  ( dom X u. dom ( _I |` ( dom X u. ran X ) ) ) C_ ( dom X u. ran X )
82 77 81 eqsstri 
 |-  dom ( X u. ( _I |` ( dom X u. ran X ) ) ) C_ ( dom X u. ran X )
83 rnun 
 |-  ran ( X u. ( _I |` ( dom X u. ran X ) ) ) = ( ran X u. ran ( _I |` ( dom X u. ran X ) ) )
84 ssun2 
 |-  ran X C_ ( dom X u. ran X )
85 rnresi 
 |-  ran ( _I |` ( dom X u. ran X ) ) = ( dom X u. ran X )
86 85 eqimssi 
 |-  ran ( _I |` ( dom X u. ran X ) ) C_ ( dom X u. ran X )
87 84 86 unssi 
 |-  ( ran X u. ran ( _I |` ( dom X u. ran X ) ) ) C_ ( dom X u. ran X )
88 83 87 eqsstri 
 |-  ran ( X u. ( _I |` ( dom X u. ran X ) ) ) C_ ( dom X u. ran X )
89 82 88 pm3.2i 
 |-  ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) C_ ( dom X u. ran X ) /\ ran ( X u. ( _I |` ( dom X u. ran X ) ) ) C_ ( dom X u. ran X ) )
90 unss 
 |-  ( ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) C_ ( dom X u. ran X ) /\ ran ( X u. ( _I |` ( dom X u. ran X ) ) ) C_ ( dom X u. ran X ) ) <-> ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) u. ran ( X u. ( _I |` ( dom X u. ran X ) ) ) ) C_ ( dom X u. ran X ) )
91 ssres2 
 |-  ( ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) u. ran ( X u. ( _I |` ( dom X u. ran X ) ) ) ) C_ ( dom X u. ran X ) -> ( _I |` ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) u. ran ( X u. ( _I |` ( dom X u. ran X ) ) ) ) ) C_ ( _I |` ( dom X u. ran X ) ) )
92 90 91 sylbi 
 |-  ( ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) C_ ( dom X u. ran X ) /\ ran ( X u. ( _I |` ( dom X u. ran X ) ) ) C_ ( dom X u. ran X ) ) -> ( _I |` ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) u. ran ( X u. ( _I |` ( dom X u. ran X ) ) ) ) ) C_ ( _I |` ( dom X u. ran X ) ) )
93 ssun4 
 |-  ( ( _I |` ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) u. ran ( X u. ( _I |` ( dom X u. ran X ) ) ) ) ) C_ ( _I |` ( dom X u. ran X ) ) -> ( _I |` ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) u. ran ( X u. ( _I |` ( dom X u. ran X ) ) ) ) ) C_ ( X u. ( _I |` ( dom X u. ran X ) ) ) )
94 89 92 93 mp2b 
 |-  ( _I |` ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) u. ran ( X u. ( _I |` ( dom X u. ran X ) ) ) ) ) C_ ( X u. ( _I |` ( dom X u. ran X ) ) )
95 94 a1i 
 |-  ( X e. V -> ( _I |` ( dom ( X u. ( _I |` ( dom X u. ran X ) ) ) u. ran ( X u. ( _I |` ( dom X u. ran X ) ) ) ) ) C_ ( X u. ( _I |` ( dom X u. ran X ) ) ) )
96 44 61 67 69 76 95 clcnvlem 
 |-  ( X e. V -> `' |^| { x | ( X C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) } = |^| { y | ( `' X C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) } )