Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  clcnvlem Structured version   Visualization version   Unicode version

Theorem clcnvlem 36230
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.)
Hypotheses
Ref Expression
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
Ref Expression
clcnvlem  |-  ( ph  ->  `' |^| { x  |  ( X  C_  x  /\  ps ) }  =  |^| { y  |  ( `' X  C_  y  /\  ch ) } )
Distinct variable groups:    x, A    x, y, X    ph, x, y    ps, y    ch, x    th, x
Allowed substitution hints:    ps( x)    ch( y)    th( y)    A( y)

Proof of Theorem clcnvlem
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 clcnvlem.ubex . . . 4  |-  ( ph  ->  A  e.  _V )
2 clcnvlem.ssub . . . . 5  |-  ( ph  ->  X  C_  A )
3 clcnvlem.clex . . . . 5  |-  ( ph  ->  th )
42, 3jca 535 . . . 4  |-  ( ph  ->  ( X  C_  A  /\  th ) )
5 clcnvlem.sub3 . . . . 5  |-  ( x  =  A  ->  ( ps 
<->  th ) )
65cleq2lem 36214 . . . 4  |-  ( x  =  A  ->  (
( X  C_  x  /\  ps )  <->  ( X  C_  A  /\  th )
) )
71, 4, 6elabd 36178 . . 3  |-  ( ph  ->  E. x ( X 
C_  x  /\  ps ) )
87cnvintabd 36209 . 2  |-  ( ph  ->  `' |^| { x  |  ( X  C_  x  /\  ps ) }  =  |^| { z  e.  ~P ( _V  X.  _V )  |  E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) } )
9 df-rab 2746 . . . . 5  |-  { 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 ) ) ) }
10 exsimpl 1729 . . . . . . . . . . 11  |-  ( E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) )  ->  E. x  z  =  `' x
)
11 relcnv 5207 . . . . . . . . . . . . 13  |-  Rel  `' x
12 releq 4917 . . . . . . . . . . . . 13  |-  ( z  =  `' x  -> 
( Rel  z  <->  Rel  `' x
) )
1311, 12mpbiri 237 . . . . . . . . . . . 12  |-  ( z  =  `' x  ->  Rel  z )
1413exlimiv 1776 . . . . . . . . . . 11  |-  ( E. x  z  =  `' x  ->  Rel  z )
1510, 14syl 17 . . . . . . . . . 10  |-  ( E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) )  ->  Rel  z )
16 df-rel 4841 . . . . . . . . . 10  |-  ( Rel  z  <->  z  C_  ( _V  X.  _V ) )
1715, 16sylib 200 . . . . . . . . 9  |-  ( E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) )  ->  z  C_  ( _V  X.  _V ) )
18 selpw 3958 . . . . . . . . . 10  |-  ( z  e.  ~P ( _V 
X.  _V )  <->  z  C_  ( _V  X.  _V )
)
1918bicomi 206 . . . . . . . . 9  |-  ( z 
C_  ( _V  X.  _V )  <->  z  e.  ~P ( _V  X.  _V )
)
2017, 19sylib 200 . . . . . . . 8  |-  ( E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) )  ->  z  e.  ~P ( _V  X.  _V ) )
2120pm4.71ri 639 . . . . . . 7  |-  ( E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) )  <->  ( z  e.  ~P ( _V  X.  _V )  /\  E. x
( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) ) )
2221bicomi 206 . . . . . 6  |-  ( ( z  e.  ~P ( _V  X.  _V )  /\  E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) )  <->  E. x
( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) )
2322abbii 2567 . . . . 5  |-  { z  |  ( z  e. 
~P ( _V  X.  _V )  /\  E. x
( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) ) }  =  {
z  |  E. x
( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) }
249, 23eqtri 2473 . . . 4  |-  { z  e.  ~P ( _V 
X.  _V )  |  E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) }  =  { z  |  E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) }
2524inteqi 4238 . . 3  |-  |^| { z  e.  ~P ( _V 
X.  _V )  |  E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) }  =  |^| { z  |  E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) }
2625a1i 11 . 2  |-  ( ph  ->  |^| { z  e. 
~P ( _V  X.  _V )  |  E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) }  =  |^| { z  |  E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) } )
27 vex 3048 . . . . . . 7  |-  y  e. 
_V
2827cnvex 6740 . . . . . 6  |-  `' y  e.  _V
2928cnvex 6740 . . . . 5  |-  `' `' y  e.  _V
3029a1i 11 . . . 4  |-  ( ph  ->  `' `' y  e.  _V )
311, 2ssexd 4550 . . . . . . . . . . 11  |-  ( ph  ->  X  e.  _V )
32 difexg 4551 . . . . . . . . . . 11  |-  ( X  e.  _V  ->  ( X  \  `' `' X
)  e.  _V )
3331, 32syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( X  \  `' `' X )  e.  _V )
34 unexg 6592 . . . . . . . . . 10  |-  ( ( `' y  e.  _V  /\  ( X  \  `' `' X )  e.  _V )  ->  ( `' y  u.  ( X  \  `' `' X ) )  e. 
_V )
3528, 33, 34sylancr 669 . . . . . . . . 9  |-  ( ph  ->  ( `' y  u.  ( X  \  `' `' X ) )  e. 
_V )
36 inundif 3845 . . . . . . . . . . . . . 14  |-  ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  =  X
37 cnvun 5241 . . . . . . . . . . . . . . . . . . . . 21  |-  `' ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  =  ( `' ( X  i^i  `' `' X )  u.  `' ( X  \  `' `' X ) )
3837sseq1i 3456 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  C_  y  <->  ( `' ( X  i^i  `' `' X )  u.  `' ( X  \  `' `' X ) )  C_  y )
3938biimpi 198 . . . . . . . . . . . . . . . . . . 19  |-  ( `' ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  C_  y  ->  ( `' ( X  i^i  `' `' X
)  u.  `' ( X  \  `' `' X ) )  C_  y )
4039unssad 3611 . . . . . . . . . . . . . . . . . 18  |-  ( `' ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  C_  y  ->  `' ( X  i^i  `' `' X )  C_  y
)
41 relcnv 5207 . . . . . . . . . . . . . . . . . . . . 21  |-  Rel  `' `' X
42 relin2 4952 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Rel  `' `' X  ->  Rel  ( X  i^i  `' `' X
) )
4341, 42ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  Rel  ( X  i^i  `' `' X
)
44 dfrel2 5286 . . . . . . . . . . . . . . . . . . . 20  |-  ( Rel  ( X  i^i  `' `' X )  <->  `' `' ( X  i^i  `' `' X )  =  ( X  i^i  `' `' X ) )
4543, 44mpbi 212 . . . . . . . . . . . . . . . . . . 19  |-  `' `' ( X  i^i  `' `' X )  =  ( X  i^i  `' `' X )
46 cnvss 5007 . . . . . . . . . . . . . . . . . . 19  |-  ( `' ( X  i^i  `' `' X )  C_  y  ->  `' `' ( X  i^i  `' `' X )  C_  `' y )
4745, 46syl5eqssr 3477 . . . . . . . . . . . . . . . . . 18  |-  ( `' ( X  i^i  `' `' X )  C_  y  ->  ( X  i^i  `' `' X )  C_  `' y )
4840, 47syl 17 . . . . . . . . . . . . . . . . 17  |-  ( `' ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  C_  y  ->  ( X  i^i  `' `' X )  C_  `' y )
49 ssid 3451 . . . . . . . . . . . . . . . . 17  |-  ( X 
\  `' `' X
)  C_  ( X  \  `' `' X )
50 unss12 3606 . . . . . . . . . . . . . . . . 17  |-  ( ( ( X  i^i  `' `' X )  C_  `' y  /\  ( X  \  `' `' X )  C_  ( X  \  `' `' X
) )  ->  (
( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  C_  ( `' y  u.  ( X  \  `' `' X
) ) )
5148, 49, 50sylancl 668 . . . . . . . . . . . . . . . 16  |-  ( `' ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  C_  y  ->  ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  C_  ( `' y  u.  ( X  \  `' `' X
) ) )
5251a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
) ) ) )
53 cnveq 5008 . . . . . . . . . . . . . . . 16  |-  ( ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  =  X  ->  `' ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  =  `' X )
5453sseq1d 3459 . . . . . . . . . . . . . . 15  |-  ( ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  =  X  ->  ( `' ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  C_  y  <->  `' X  C_  y )
)
55 sseq1 3453 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
) ) ) )
5652, 54, 553imtr3d 271 . . . . . . . . . . . . . 14  |-  ( ( ( X  i^i  `' `' X )  u.  ( X  \  `' `' X
) )  =  X  ->  ( `' X  C_  y  ->  X  C_  ( `' y  u.  ( X  \  `' `' X
) ) ) )
5736, 56ax-mp 5 . . . . . . . . . . . . 13  |-  ( `' X  C_  y  ->  X 
C_  ( `' y  u.  ( X  \  `' `' X ) ) )
58 sseq2 3454 . . . . . . . . . . . . 13  |-  ( x  =  ( `' y  u.  ( X  \  `' `' X ) )  -> 
( X  C_  x  <->  X 
C_  ( `' y  u.  ( X  \  `' `' X ) ) ) )
5957, 58syl5ibr 225 . . . . . . . . . . . 12  |-  ( x  =  ( `' y  u.  ( X  \  `' `' X ) )  -> 
( `' X  C_  y  ->  X  C_  x
) )
6059adantl 468 . . . . . . . . . . 11  |-  ( (
ph  /\  x  =  ( `' y  u.  ( X  \  `' `' X
) ) )  -> 
( `' X  C_  y  ->  X  C_  x
) )
61 clcnvlem.sub1 . . . . . . . . . . 11  |-  ( (
ph  /\  x  =  ( `' y  u.  ( X  \  `' `' X
) ) )  -> 
( ch  ->  ps ) )
6260, 61anim12d 566 . . . . . . . . . 10  |-  ( (
ph  /\  x  =  ( `' y  u.  ( X  \  `' `' X
) ) )  -> 
( ( `' X  C_  y  /\  ch )  ->  ( X  C_  x  /\  ps ) ) )
63 cnveq 5008 . . . . . . . . . . . 12  |-  ( x  =  ( `' y  u.  ( X  \  `' `' X ) )  ->  `' x  =  `' ( `' y  u.  ( X  \  `' `' X
) ) )
64 cnvun 5241 . . . . . . . . . . . . 13  |-  `' ( `' y  u.  ( X  \  `' `' X
) )  =  ( `' `' y  u.  `' ( X  \  `' `' X ) )
65 cnvnonrel 36194 . . . . . . . . . . . . . . 15  |-  `' ( X  \  `' `' X )  =  (/)
66 0ss 3763 . . . . . . . . . . . . . . 15  |-  (/)  C_  `' `' y
6765, 66eqsstri 3462 . . . . . . . . . . . . . 14  |-  `' ( X  \  `' `' X )  C_  `' `' y
68 ssequn2 3607 . . . . . . . . . . . . . 14  |-  ( `' ( X  \  `' `' X )  C_  `' `' y  <->  ( `' `' y  u.  `' ( X  \  `' `' X
) )  =  `' `' y )
6967, 68mpbi 212 . . . . . . . . . . . . 13  |-  ( `' `' y  u.  `' ( X  \  `' `' X ) )  =  `' `' y
7064, 69eqtr2i 2474 . . . . . . . . . . . 12  |-  `' `' y  =  `' ( `' y  u.  ( X  \  `' `' X
) )
7163, 70syl6reqr 2504 . . . . . . . . . . 11  |-  ( x  =  ( `' y  u.  ( X  \  `' `' X ) )  ->  `' `' y  =  `' x )
7271adantl 468 . . . . . . . . . 10  |-  ( (
ph  /\  x  =  ( `' y  u.  ( X  \  `' `' X
) ) )  ->  `' `' y  =  `' x )
7362, 72jctild 546 . . . . . . . . 9  |-  ( (
ph  /\  x  =  ( `' y  u.  ( X  \  `' `' X
) ) )  -> 
( ( `' X  C_  y  /\  ch )  ->  ( `' `' y  =  `' x  /\  ( X  C_  x  /\  ps ) ) ) )
7435, 73spcimedv 3133 . . . . . . . 8  |-  ( ph  ->  ( ( `' X  C_  y  /\  ch )  ->  E. x ( `' `' y  =  `' x  /\  ( X  C_  x  /\  ps ) ) ) )
7574imp 431 . . . . . . 7  |-  ( (
ph  /\  ( `' X  C_  y  /\  ch ) )  ->  E. x
( `' `' y  =  `' x  /\  ( X  C_  x  /\  ps ) ) )
7675adantlr 721 . . . . . 6  |-  ( ( ( ph  /\  z  =  `' `' y )  /\  ( `' X  C_  y  /\  ch ) )  ->  E. x
( `' `' y  =  `' x  /\  ( X  C_  x  /\  ps ) ) )
77 eqeq1 2455 . . . . . . . . 9  |-  ( z  =  `' `' y  ->  ( z  =  `' x  <->  `' `' y  =  `' x ) )
7877anbi1d 711 . . . . . . . 8  |-  ( z  =  `' `' y  ->  ( ( z  =  `' x  /\  ( X  C_  x  /\  ps ) )  <->  ( `' `' y  =  `' x  /\  ( X  C_  x  /\  ps ) ) ) )
7978exbidv 1768 . . . . . . 7  |-  ( z  =  `' `' y  ->  ( E. x
( z  =  `' x  /\  ( X  C_  x  /\  ps ) )  <->  E. x ( `' `' y  =  `' x  /\  ( X  C_  x  /\  ps ) ) ) )
8079ad2antlr 733 . . . . . 6  |-  ( ( ( ph  /\  z  =  `' `' y )  /\  ( `' X  C_  y  /\  ch ) )  ->  ( E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) )  <->  E. x
( `' `' y  =  `' x  /\  ( X  C_  x  /\  ps ) ) ) )
8176, 80mpbird 236 . . . . 5  |-  ( ( ( ph  /\  z  =  `' `' y )  /\  ( `' X  C_  y  /\  ch ) )  ->  E. x
( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) )
8281ex 436 . . . 4  |-  ( (
ph  /\  z  =  `' `' y )  -> 
( ( `' X  C_  y  /\  ch )  ->  E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) ) )
83 cnvcnvss 5290 . . . . 5  |-  `' `' y  C_  y
8483a1i 11 . . . 4  |-  ( ph  ->  `' `' y  C_  y )
8530, 82, 84intabssd 36216 . . 3  |-  ( ph  ->  |^| { z  |  E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) }  C_  |^|
{ y  |  ( `' X  C_  y  /\  ch ) } )
86 vex 3048 . . . . 5  |-  z  e. 
_V
8786a1i 11 . . . 4  |-  ( ph  ->  z  e.  _V )
88 eqtr 2470 . . . . . . . 8  |-  ( ( y  =  z  /\  z  =  `' x
)  ->  y  =  `' x )
89 cnvss 5007 . . . . . . . . . . . 12  |-  ( X 
C_  x  ->  `' X  C_  `' x )
90 sseq2 3454 . . . . . . . . . . . 12  |-  ( y  =  `' x  -> 
( `' X  C_  y 
<->  `' X  C_  `' x
) )
9189, 90syl5ibr 225 . . . . . . . . . . 11  |-  ( y  =  `' x  -> 
( X  C_  x  ->  `' X  C_  y ) )
9291adantl 468 . . . . . . . . . 10  |-  ( (
ph  /\  y  =  `' x )  ->  ( X  C_  x  ->  `' X  C_  y ) )
93 clcnvlem.sub2 . . . . . . . . . 10  |-  ( (
ph  /\  y  =  `' x )  ->  ( ps  ->  ch ) )
9492, 93anim12d 566 . . . . . . . . 9  |-  ( (
ph  /\  y  =  `' x )  ->  (
( X  C_  x  /\  ps )  ->  ( `' X  C_  y  /\  ch ) ) )
9594ex 436 . . . . . . . 8  |-  ( ph  ->  ( y  =  `' x  ->  ( ( X 
C_  x  /\  ps )  ->  ( `' X  C_  y  /\  ch )
) ) )
9688, 95syl5 33 . . . . . . 7  |-  ( ph  ->  ( ( y  =  z  /\  z  =  `' x )  ->  (
( X  C_  x  /\  ps )  ->  ( `' X  C_  y  /\  ch ) ) ) )
9796impl 626 . . . . . 6  |-  ( ( ( ph  /\  y  =  z )  /\  z  =  `' x
)  ->  ( ( X  C_  x  /\  ps )  ->  ( `' X  C_  y  /\  ch )
) )
9897expimpd 608 . . . . 5  |-  ( (
ph  /\  y  =  z )  ->  (
( z  =  `' x  /\  ( X  C_  x  /\  ps ) )  ->  ( `' X  C_  y  /\  ch )
) )
9998exlimdv 1779 . . . 4  |-  ( (
ph  /\  y  =  z )  ->  ( E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) )  ->  ( `' X  C_  y  /\  ch ) ) )
100 ssid 3451 . . . . 5  |-  z  C_  z
101100a1i 11 . . . 4  |-  ( ph  ->  z  C_  z )
10287, 99, 101intabssd 36216 . . 3  |-  ( ph  ->  |^| { y  |  ( `' X  C_  y  /\  ch ) } 
C_  |^| { z  |  E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) } )
10385, 102eqssd 3449 . 2  |-  ( ph  ->  |^| { z  |  E. x ( z  =  `' x  /\  ( X  C_  x  /\  ps ) ) }  =  |^| { y  |  ( `' X  C_  y  /\  ch ) } )
1048, 26, 1033eqtrd 2489 1  |-  ( ph  ->  `' |^| { x  |  ( X  C_  x  /\  ps ) }  =  |^| { y  |  ( `' X  C_  y  /\  ch ) } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1444   E.wex 1663    e. wcel 1887   {cab 2437   {crab 2741   _Vcvv 3045    \ cdif 3401    u. cun 3402    i^i cin 3403    C_ wss 3404   (/)c0 3731   ~Pcpw 3951   |^|cint 4234    X. cxp 4832   `'ccnv 4833   Rel wrel 4839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-int 4235  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-iota 5546  df-fun 5584  df-fv 5590  df-1st 6793  df-2nd 6794
This theorem is referenced by:  cnvtrucl0  36231  cnvrcl0  36232  cnvtrcl0  36233
  Copyright terms: Public domain W3C validator