Metamath Proof Explorer

Theorem clcnvlem

Description: When A , an upper bound of the closure, exists and certain substitutions hold the converse of the closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020)

Ref Expression
Hypotheses clcnvlem.sub1 
|- ( ( ph /\ x = ( `' y u. ( X \ `' `' X ) ) ) -> ( ch -> ps ) )
clcnvlem.sub2 
|- ( ( ph /\ y = `' x ) -> ( ps -> ch ) )
clcnvlem.sub3 
|- ( x = A -> ( ps <-> th ) )
clcnvlem.ssub 
|- ( ph -> X C_ A )
clcnvlem.ubex 
|- ( ph -> A e. _V )
clcnvlem.clex 
|- ( ph -> th )
Assertion clcnvlem 
|- ( ph -> `' |^| { x | ( X C_ x /\ ps ) } = |^| { y | ( `' X C_ y /\ ch ) } )

Proof

Step Hyp Ref Expression
1 clcnvlem.sub1 
 |-  ( ( ph /\ x = ( `' y u. ( X \ `' `' X ) ) ) -> ( ch -> ps ) )
2 clcnvlem.sub2 
 |-  ( ( ph /\ y = `' x ) -> ( ps -> ch ) )
3 clcnvlem.sub3 
 |-  ( x = A -> ( ps <-> th ) )
4 clcnvlem.ssub 
 |-  ( ph -> X C_ A )
5 clcnvlem.ubex 
 |-  ( ph -> A e. _V )
6 clcnvlem.clex 
 |-  ( ph -> th )
7 4 6 jca 
 |-  ( ph -> ( X C_ A /\ th ) )
8 3 cleq2lem 
 |-  ( x = A -> ( ( X C_ x /\ ps ) <-> ( X C_ A /\ th ) ) )
9 5 7 8 spcedv 
 |-  ( ph -> E. x ( X C_ x /\ ps ) )
10 9 cnvintabd 
 |-  ( ph -> `' |^| { x | ( X C_ x /\ ps ) } = |^| { z e. ~P ( _V X. _V ) | E. x ( z = `' x /\ ( X C_ x /\ ps ) ) } )
11 df-rab 
 |-  { z e. ~P ( _V X. _V ) | E. x ( z = `' x /\ ( X C_ x /\ ps ) ) } = { z | ( z e. ~P ( _V X. _V ) /\ E. x ( z = `' x /\ ( X C_ x /\ ps ) ) ) }
12 exsimpl 
 |-  ( E. x ( z = `' x /\ ( X C_ x /\ ps ) ) -> E. x z = `' x )
13 relcnv 
 |-  Rel `' x
14 releq 
 |-  ( z = `' x -> ( Rel z <-> Rel `' x ) )
15 13 14 mpbiri 
 |-  ( z = `' x -> Rel z )
16 15 exlimiv 
 |-  ( E. x z = `' x -> Rel z )
17 12 16 syl 
 |-  ( E. x ( z = `' x /\ ( X C_ x /\ ps ) ) -> Rel z )
18 df-rel 
 |-  ( Rel z <-> z C_ ( _V X. _V ) )
19 17 18 sylib 
 |-  ( E. x ( z = `' x /\ ( X C_ x /\ ps ) ) -> z C_ ( _V X. _V ) )
20 velpw 
 |-  ( z e. ~P ( _V X. _V ) <-> z C_ ( _V X. _V ) )
21 20 bicomi 
 |-  ( z C_ ( _V X. _V ) <-> z e. ~P ( _V X. _V ) )
22 19 21 sylib 
 |-  ( E. x ( z = `' x /\ ( X C_ x /\ ps ) ) -> z e. ~P ( _V X. _V ) )
23 22 pm4.71ri 
 |-  ( E. x ( z = `' x /\ ( X C_ x /\ ps ) ) <-> ( z e. ~P ( _V X. _V ) /\ E. x ( z = `' x /\ ( X C_ x /\ ps ) ) ) )
24 23 bicomi 
 |-  ( ( z e. ~P ( _V X. _V ) /\ E. x ( z = `' x /\ ( X C_ x /\ ps ) ) ) <-> E. x ( z = `' x /\ ( X C_ x /\ ps ) ) )
25 24 abbii 
 |-  { z | ( z e. ~P ( _V X. _V ) /\ E. x ( z = `' x /\ ( X C_ x /\ ps ) ) ) } = { z | E. x ( z = `' x /\ ( X C_ x /\ ps ) ) }
26 11 25 eqtri 
 |-  { z e. ~P ( _V X. _V ) | E. x ( z = `' x /\ ( X C_ x /\ ps ) ) } = { z | E. x ( z = `' x /\ ( X C_ x /\ ps ) ) }
27 26 inteqi 
 |-  |^| { z e. ~P ( _V X. _V ) | E. x ( z = `' x /\ ( X C_ x /\ ps ) ) } = |^| { z | E. x ( z = `' x /\ ( X C_ x /\ ps ) ) }
28 27 a1i 
 |-  ( ph -> |^| { z e. ~P ( _V X. _V ) | E. x ( z = `' x /\ ( X C_ x /\ ps ) ) } = |^| { z | E. x ( z = `' x /\ ( X C_ x /\ ps ) ) } )
29 vex 
 |-  y e. _V
30 29 cnvex 
 |-  `' y e. _V
31 30 cnvex 
 |-  `' `' y e. _V
32 31 a1i 
 |-  ( ph -> `' `' y e. _V )
33 5 4 ssexd 
 |-  ( ph -> X e. _V )
34 33 difexd 
 |-  ( ph -> ( X \ `' `' X ) e. _V )
35 unexg 
 |-  ( ( `' y e. _V /\ ( X \ `' `' X ) e. _V ) -> ( `' y u. ( X \ `' `' X ) ) e. _V )
36 30 34 35 sylancr 
 |-  ( ph -> ( `' y u. ( X \ `' `' X ) ) e. _V )
37 inundif 
 |-  ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) = X
38 cnvun 
 |-  `' ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) = ( `' ( X i^i `' `' X ) u. `' ( X \ `' `' X ) )
39 38 sseq1i 
 |-  ( `' ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) C_ y <-> ( `' ( X i^i `' `' X ) u. `' ( X \ `' `' X ) ) C_ y )
40 39 biimpi 
 |-  ( `' ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) C_ y -> ( `' ( X i^i `' `' X ) u. `' ( X \ `' `' X ) ) C_ y )
41 40 unssad 
 |-  ( `' ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) C_ y -> `' ( X i^i `' `' X ) C_ y )
42 relcnv 
 |-  Rel `' `' X
43 relin2 
 |-  ( Rel `' `' X -> Rel ( X i^i `' `' X ) )
44 42 43 ax-mp 
 |-  Rel ( X i^i `' `' X )
45 dfrel2 
 |-  ( Rel ( X i^i `' `' X ) <-> `' `' ( X i^i `' `' X ) = ( X i^i `' `' X ) )
46 44 45 mpbi 
 |-  `' `' ( X i^i `' `' X ) = ( X i^i `' `' X )
47 cnvss 
 |-  ( `' ( X i^i `' `' X ) C_ y -> `' `' ( X i^i `' `' X ) C_ `' y )
48 46 47 eqsstrrid 
 |-  ( `' ( X i^i `' `' X ) C_ y -> ( X i^i `' `' X ) C_ `' y )
49 41 48 syl 
 |-  ( `' ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) C_ y -> ( X i^i `' `' X ) C_ `' y )
50 ssid 
 |-  ( X \ `' `' X ) C_ ( X \ `' `' X )
51 unss12 
 |-  ( ( ( X i^i `' `' X ) C_ `' y /\ ( X \ `' `' X ) C_ ( X \ `' `' X ) ) -> ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) C_ ( `' y u. ( X \ `' `' X ) ) )
52 49 50 51 sylancl 
 |-  ( `' ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) C_ y -> ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) C_ ( `' y u. ( X \ `' `' X ) ) )
53 52 a1i 
 |-  ( ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) = X -> ( `' ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) C_ y -> ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) C_ ( `' y u. ( X \ `' `' X ) ) ) )
54 cnveq 
 |-  ( ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) = X -> `' ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) = `' X )
55 54 sseq1d 
 |-  ( ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) = X -> ( `' ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) C_ y <-> `' X C_ y ) )
56 sseq1 
 |-  ( ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) = X -> ( ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) C_ ( `' y u. ( X \ `' `' X ) ) <-> X C_ ( `' y u. ( X \ `' `' X ) ) ) )
57 53 55 56 3imtr3d 
 |-  ( ( ( X i^i `' `' X ) u. ( X \ `' `' X ) ) = X -> ( `' X C_ y -> X C_ ( `' y u. ( X \ `' `' X ) ) ) )
58 37 57 ax-mp 
 |-  ( `' X C_ y -> X C_ ( `' y u. ( X \ `' `' X ) ) )
59 sseq2 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> ( X C_ x <-> X C_ ( `' y u. ( X \ `' `' X ) ) ) )
60 58 59 syl5ibr 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> ( `' X C_ y -> X C_ x ) )
61 60 adantl 
 |-  ( ( ph /\ x = ( `' y u. ( X \ `' `' X ) ) ) -> ( `' X C_ y -> X C_ x ) )
62 61 1 anim12d 
 |-  ( ( ph /\ x = ( `' y u. ( X \ `' `' X ) ) ) -> ( ( `' X C_ y /\ ch ) -> ( X C_ x /\ ps ) ) )
63 cnvun 
 |-  `' ( `' y u. ( X \ `' `' X ) ) = ( `' `' y u. `' ( X \ `' `' X ) )
64 cnvnonrel 
 |-  `' ( X \ `' `' X ) = (/)
65 0ss 
 |-  (/) C_ `' `' y
66 64 65 eqsstri 
 |-  `' ( X \ `' `' X ) C_ `' `' y
67 ssequn2 
 |-  ( `' ( X \ `' `' X ) C_ `' `' y <-> ( `' `' y u. `' ( X \ `' `' X ) ) = `' `' y )
68 66 67 mpbi 
 |-  ( `' `' y u. `' ( X \ `' `' X ) ) = `' `' y
69 63 68 eqtr2i 
 |-  `' `' y = `' ( `' y u. ( X \ `' `' X ) )
70 cnveq 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> `' x = `' ( `' y u. ( X \ `' `' X ) ) )
71 69 70 eqtr4id 
 |-  ( x = ( `' y u. ( X \ `' `' X ) ) -> `' `' y = `' x )
72 71 adantl 
 |-  ( ( ph /\ x = ( `' y u. ( X \ `' `' X ) ) ) -> `' `' y = `' x )
73 62 72 jctild 
 |-  ( ( ph /\ x = ( `' y u. ( X \ `' `' X ) ) ) -> ( ( `' X C_ y /\ ch ) -> ( `' `' y = `' x /\ ( X C_ x /\ ps ) ) ) )
74 36 73 spcimedv 
 |-  ( ph -> ( ( `' X C_ y /\ ch ) -> E. x ( `' `' y = `' x /\ ( X C_ x /\ ps ) ) ) )
75 74 imp 
 |-  ( ( ph /\ ( `' X C_ y /\ ch ) ) -> E. x ( `' `' y = `' x /\ ( X C_ x /\ ps ) ) )
76 75 adantlr 
 |-  ( ( ( ph /\ z = `' `' y ) /\ ( `' X C_ y /\ ch ) ) -> E. x ( `' `' y = `' x /\ ( X C_ x /\ ps ) ) )
77 eqeq1 
 |-  ( z = `' `' y -> ( z = `' x <-> `' `' y = `' x ) )
78 77 anbi1d 
 |-  ( z = `' `' y -> ( ( z = `' x /\ ( X C_ x /\ ps ) ) <-> ( `' `' y = `' x /\ ( X C_ x /\ ps ) ) ) )
79 78 exbidv 
 |-  ( z = `' `' y -> ( E. x ( z = `' x /\ ( X C_ x /\ ps ) ) <-> E. x ( `' `' y = `' x /\ ( X C_ x /\ ps ) ) ) )
80 79 ad2antlr 
 |-  ( ( ( ph /\ z = `' `' y ) /\ ( `' X C_ y /\ ch ) ) -> ( E. x ( z = `' x /\ ( X C_ x /\ ps ) ) <-> E. x ( `' `' y = `' x /\ ( X C_ x /\ ps ) ) ) )
81 76 80 mpbird 
 |-  ( ( ( ph /\ z = `' `' y ) /\ ( `' X C_ y /\ ch ) ) -> E. x ( z = `' x /\ ( X C_ x /\ ps ) ) )
82 81 ex 
 |-  ( ( ph /\ z = `' `' y ) -> ( ( `' X C_ y /\ ch ) -> E. x ( z = `' x /\ ( X C_ x /\ ps ) ) ) )
83 cnvcnvss 
 |-  `' `' y C_ y
84 83 a1i 
 |-  ( ph -> `' `' y C_ y )
85 32 82 84 intabssd 
 |-  ( ph -> |^| { z | E. x ( z = `' x /\ ( X C_ x /\ ps ) ) } C_ |^| { y | ( `' X C_ y /\ ch ) } )
86 vex 
 |-  z e. _V
87 86 a1i 
 |-  ( ph -> z e. _V )
88 eqtr 
 |-  ( ( y = z /\ z = `' x ) -> y = `' x )
89 cnvss 
 |-  ( X C_ x -> `' X C_ `' x )
90 sseq2 
 |-  ( y = `' x -> ( `' X C_ y <-> `' X C_ `' x ) )
91 89 90 syl5ibr 
 |-  ( y = `' x -> ( X C_ x -> `' X C_ y ) )
92 91 adantl 
 |-  ( ( ph /\ y = `' x ) -> ( X C_ x -> `' X C_ y ) )
93 92 2 anim12d 
 |-  ( ( ph /\ y = `' x ) -> ( ( X C_ x /\ ps ) -> ( `' X C_ y /\ ch ) ) )
94 93 ex 
 |-  ( ph -> ( y = `' x -> ( ( X C_ x /\ ps ) -> ( `' X C_ y /\ ch ) ) ) )
95 88 94 syl5 
 |-  ( ph -> ( ( y = z /\ z = `' x ) -> ( ( X C_ x /\ ps ) -> ( `' X C_ y /\ ch ) ) ) )
96 95 impl 
 |-  ( ( ( ph /\ y = z ) /\ z = `' x ) -> ( ( X C_ x /\ ps ) -> ( `' X C_ y /\ ch ) ) )
97 96 expimpd 
 |-  ( ( ph /\ y = z ) -> ( ( z = `' x /\ ( X C_ x /\ ps ) ) -> ( `' X C_ y /\ ch ) ) )
98 97 exlimdv 
 |-  ( ( ph /\ y = z ) -> ( E. x ( z = `' x /\ ( X C_ x /\ ps ) ) -> ( `' X C_ y /\ ch ) ) )
99 ssid 
 |-  z C_ z
100 99 a1i 
 |-  ( ph -> z C_ z )
101 87 98 100 intabssd 
 |-  ( ph -> |^| { y | ( `' X C_ y /\ ch ) } C_ |^| { z | E. x ( z = `' x /\ ( X C_ x /\ ps ) ) } )
102 85 101 eqssd 
 |-  ( ph -> |^| { z | E. x ( z = `' x /\ ( X C_ x /\ ps ) ) } = |^| { y | ( `' X C_ y /\ ch ) } )
103 10 28 102 3eqtrd 
 |-  ( ph -> `' |^| { x | ( X C_ x /\ ps ) } = |^| { y | ( `' X C_ y /\ ch ) } )