Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cnvoprab Structured version   Visualization version   Unicode version

Theorem cnvoprab 28308
Description: The converse of a class abstraction of nested ordered pairs. (Contributed by Thierry Arnoux, 17-Aug-2017.)
Hypotheses
Ref Expression
cnvoprab.x  |-  F/ x ps
cnvoprab.y  |-  F/ y ps
cnvoprab.1  |-  ( a  =  <. x ,  y
>.  ->  ( ps  <->  ph ) )
cnvoprab.2  |-  ( ps 
->  a  e.  ( _V  X.  _V ) )
Assertion
Ref Expression
cnvoprab  |-  `' { <. <. x ,  y
>. ,  z >.  | 
ph }  =  { <. z ,  a >.  |  ps }
Distinct variable groups:    x, a,
y, z    ph, a
Allowed substitution hints:    ph( x, y, z)    ps( x, y, z, a)

Proof of Theorem cnvoprab
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 excom 1927 . . . . . 6  |-  ( E. a E. z ( w  =  <. a ,  z >.  /\  ps ) 
<->  E. z E. a
( w  =  <. a ,  z >.  /\  ps ) )
2 nfv 1761 . . . . . . . . . . 11  |-  F/ x  w  =  <. a ,  z >.
3 cnvoprab.x . . . . . . . . . . 11  |-  F/ x ps
42, 3nfan 2011 . . . . . . . . . 10  |-  F/ x
( w  =  <. a ,  z >.  /\  ps )
54nfex 2031 . . . . . . . . 9  |-  F/ x E. a ( w  = 
<. a ,  z >.  /\  ps )
6 nfv 1761 . . . . . . . . . . . 12  |-  F/ y  w  =  <. a ,  z >.
7 cnvoprab.y . . . . . . . . . . . 12  |-  F/ y ps
86, 7nfan 2011 . . . . . . . . . . 11  |-  F/ y ( w  =  <. a ,  z >.  /\  ps )
98nfex 2031 . . . . . . . . . 10  |-  F/ y E. a ( w  =  <. a ,  z
>.  /\  ps )
10 opex 4664 . . . . . . . . . . 11  |-  <. x ,  y >.  e.  _V
11 opeq1 4166 . . . . . . . . . . . . 13  |-  ( a  =  <. x ,  y
>.  ->  <. a ,  z
>.  =  <. <. x ,  y >. ,  z
>. )
1211eqeq2d 2461 . . . . . . . . . . . 12  |-  ( a  =  <. x ,  y
>.  ->  ( w  = 
<. a ,  z >.  <->  w  =  <. <. x ,  y
>. ,  z >. ) )
13 cnvoprab.1 . . . . . . . . . . . 12  |-  ( a  =  <. x ,  y
>.  ->  ( ps  <->  ph ) )
1412, 13anbi12d 717 . . . . . . . . . . 11  |-  ( a  =  <. x ,  y
>.  ->  ( ( w  =  <. a ,  z
>.  /\  ps )  <->  ( w  =  <. <. x ,  y
>. ,  z >.  /\ 
ph ) ) )
1510, 14spcev 3141 . . . . . . . . . 10  |-  ( ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph )  ->  E. a ( w  = 
<. a ,  z >.  /\  ps ) )
169, 15exlimi 1995 . . . . . . . . 9  |-  ( E. y ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )  ->  E. a
( w  =  <. a ,  z >.  /\  ps ) )
175, 16exlimi 1995 . . . . . . . 8  |-  ( E. x E. y ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph )  ->  E. a ( w  = 
<. a ,  z >.  /\  ps ) )
18 cnvoprab.2 . . . . . . . . . . 11  |-  ( ps 
->  a  e.  ( _V  X.  _V ) )
1918adantl 468 . . . . . . . . . 10  |-  ( ( w  =  <. a ,  z >.  /\  ps )  ->  a  e.  ( _V  X.  _V )
)
20 fvex 5875 . . . . . . . . . . 11  |-  ( 1st `  a )  e.  _V
21 fvex 5875 . . . . . . . . . . 11  |-  ( 2nd `  a )  e.  _V
22 eqcom 2458 . . . . . . . . . . . . . . 15  |-  ( ( 1st `  a )  =  x  <->  x  =  ( 1st `  a ) )
23 eqcom 2458 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  a )  =  y  <->  y  =  ( 2nd `  a ) )
2422, 23anbi12i 703 . . . . . . . . . . . . . 14  |-  ( ( ( 1st `  a
)  =  x  /\  ( 2nd `  a )  =  y )  <->  ( x  =  ( 1st `  a
)  /\  y  =  ( 2nd `  a ) ) )
25 eqopi 6827 . . . . . . . . . . . . . 14  |-  ( ( a  e.  ( _V 
X.  _V )  /\  (
( 1st `  a
)  =  x  /\  ( 2nd `  a )  =  y ) )  ->  a  =  <. x ,  y >. )
2624, 25sylan2br 479 . . . . . . . . . . . . 13  |-  ( ( a  e.  ( _V 
X.  _V )  /\  (
x  =  ( 1st `  a )  /\  y  =  ( 2nd `  a
) ) )  -> 
a  =  <. x ,  y >. )
2714bicomd 205 . . . . . . . . . . . . 13  |-  ( a  =  <. x ,  y
>.  ->  ( ( w  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )  <->  ( w  =  <. a ,  z
>.  /\  ps ) ) )
2826, 27syl 17 . . . . . . . . . . . 12  |-  ( ( a  e.  ( _V 
X.  _V )  /\  (
x  =  ( 1st `  a )  /\  y  =  ( 2nd `  a
) ) )  -> 
( ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )  <->  ( w  =  <. a ,  z
>.  /\  ps ) ) )
294, 8, 28spc2ed 28106 . . . . . . . . . . 11  |-  ( ( a  e.  ( _V 
X.  _V )  /\  (
( 1st `  a
)  e.  _V  /\  ( 2nd `  a )  e.  _V ) )  ->  ( ( w  =  <. a ,  z
>.  /\  ps )  ->  E. x E. y ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph ) ) )
3020, 21, 29mpanr12 691 . . . . . . . . . 10  |-  ( a  e.  ( _V  X.  _V )  ->  ( ( w  =  <. a ,  z >.  /\  ps )  ->  E. x E. y
( w  =  <. <.
x ,  y >. ,  z >.  /\  ph ) ) )
3119, 30mpcom 37 . . . . . . . . 9  |-  ( ( w  =  <. a ,  z >.  /\  ps )  ->  E. x E. y
( w  =  <. <.
x ,  y >. ,  z >.  /\  ph ) )
3231exlimiv 1776 . . . . . . . 8  |-  ( E. a ( w  = 
<. a ,  z >.  /\  ps )  ->  E. x E. y ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) )
3317, 32impbii 191 . . . . . . 7  |-  ( E. x E. y ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph )  <->  E. a
( w  =  <. a ,  z >.  /\  ps ) )
3433exbii 1718 . . . . . 6  |-  ( E. z E. x E. y ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )  <->  E. z E. a ( w  = 
<. a ,  z >.  /\  ps ) )
35 exrot3 1931 . . . . . 6  |-  ( E. z E. x E. y ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )  <->  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph ) )
361, 34, 353bitr2ri 278 . . . . 5  |-  ( E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )  <->  E. a E. z ( w  = 
<. a ,  z >.  /\  ps ) )
3736abbii 2567 . . . 4  |-  { w  |  E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }  =  { w  |  E. a E. z ( w  =  <. a ,  z
>.  /\  ps ) }
38 df-oprab 6294 . . . 4  |-  { <. <.
x ,  y >. ,  z >.  |  ph }  =  { w  |  E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }
39 df-opab 4462 . . . 4  |-  { <. a ,  z >.  |  ps }  =  { w  |  E. a E. z
( w  =  <. a ,  z >.  /\  ps ) }
4037, 38, 393eqtr4ri 2484 . . 3  |-  { <. a ,  z >.  |  ps }  =  { <. <. x ,  y >. ,  z
>.  |  ph }
4140cnveqi 5009 . 2  |-  `' { <. a ,  z >.  |  ps }  =  `' { <. <. x ,  y
>. ,  z >.  | 
ph }
42 cnvopab 5237 . 2  |-  `' { <. a ,  z >.  |  ps }  =  { <. z ,  a >.  |  ps }
4341, 42eqtr3i 2475 1  |-  `' { <. <. x ,  y
>. ,  z >.  | 
ph }  =  { <. z ,  a >.  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1444   E.wex 1663   F/wnf 1667    e. wcel 1887   {cab 2437   _Vcvv 3045   <.cop 3974   {copab 4460    X. cxp 4832   `'ccnv 4833   ` cfv 5582   {coprab 6291   1stc1st 6791   2ndc2nd 6792
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-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  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-oprab 6294  df-1st 6793  df-2nd 6794
This theorem is referenced by:  f1od2  28309
  Copyright terms: Public domain W3C validator