Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  relopabVD Structured version   Visualization version   Unicode version

Theorem relopabVD 37295
Description: Virtual deduction proof of relopab 4938. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. relopab 4938 is relopabVD 37295 without virtual deductions and was automatically derived from relopabVD 37295.
1::  |-  (. y  =  v  ->.  y  =  v ).
2:1:  |-  (. y  =  v  ->.  <. x ,. y >.  =  <. x ,. v  >. ).
3::  |-  (. y  =  v ,. x  =  u  ->.  x  =  u ).
4:3:  |-  (. y  =  v ,. x  =  u  ->.  <. x ,. v >.  =  <.  u ,  v >. ).
5:2,4:  |-  (. y  =  v ,. x  =  u  ->.  <. x ,. y >.  =  <.  u ,  v >. ).
6:5:  |-  (. y  =  v ,. x  =  u  ->.  ( z  =  <. x ,. y  >.  ->  z  =  <. u ,  v >. ) ).
7:6:  |-  (. y  =  v  ->.  ( x  =  u  ->  ( z  =  <. x ,.  y >.  ->  z  =  <. u ,  v >. ) ) ).
8:7:  |-  ( y  =  v  ->  ( x  =  u  ->  ( z  =  <. x ,. y  >.  ->  z  =  <. u ,  v >. ) ) )
9:8:  |-  ( E. v y  =  v  ->  E. v ( x  =  u  ->  ( z  =  <. x ,  y >.  ->  z  =  <. u ,  v >. ) ) )
90::  |-  ( v  =  y  <->  y  =  v )
91:90:  |-  ( E. v v  =  y  <->  E. v y  =  v )
92::  |-  E. v v  =  y
10:91,92:  |-  E. v y  =  v
11:9,10:  |-  E. v ( x  =  u  ->  ( z  =  <. x ,. y >.  ->  z  =  <. u ,  v >. ) )
12:11:  |-  ( x  =  u  ->  E. v ( z  =  <. x ,. y >.  ->  z  =  <. u ,  v >. ) )
13::  |-  ( E. v ( z  =  <. x ,. y >.  ->  z  =  <. u  ,  v >. )  ->  ( z  =  <. x ,  y >.  ->  E. v z  =  <. u ,  v >. ) )
14:12,13:  |-  ( x  =  u  ->  ( z  =  <. x ,. y >.  ->  E. v  z  =  <. u ,  v >. ) )
15:14:  |-  ( E. u x  =  u  ->  E. u ( z  =  <. x ,. y  >.  ->  E. v z  =  <. u ,  v >. ) )
150::  |-  ( u  =  x  <->  x  =  u )
151:150:  |-  ( E. u u  =  x  <->  E. u x  =  u )
152::  |-  E. u u  =  x
16:151,152:  |-  E. u x  =  u
17:15,16:  |-  E. u ( z  =  <. x ,. y >.  ->  E. v z  =  <.  u ,  v >. )
18:17:  |-  ( z  =  <. x ,. y >.  ->  E. u E. v z  =  <.  u ,  v >. )
19:18:  |-  ( E. y z  =  <. x ,. y >.  ->  E. y E. u  E. v z  =  <. u ,  v >. )
20::  |-  ( E. y E. u E. v z  =  <. u ,. v >.  ->  E. u E. v z  =  <. u ,  v >. )
21:19,20:  |-  ( E. y z  =  <. x ,. y >.  ->  E. u E. v z  =  <. u ,  v >. )
22:21:  |-  ( E. x E. y z  =  <. x ,. y >.  ->  E. x  E. u E. v z  =  <. u ,  v >. )
23::  |-  ( E. x E. u E. v z  =  <. u ,. v >.  ->  E. u E. v z  =  <. u ,  v >. )
24:22,23:  |-  ( E. x E. y z  =  <. x ,. y >.  ->  E. u  E. v z  =  <. u ,  v >. )
25:24:  |-  { z  |  E. x E. y z  =  <. x ,. y >. }  C_  { z  |  E. u E. v z  =  <. u ,  v >. }
26::  |-  x  e.  _V
27::  |-  y  e.  _V
28:26,27:  |-  ( x  e.  _V  /\  y  e.  _V )
29:28:  |-  ( z  =  <. x ,. y >.  <->  ( z  =  <. x ,. y  >.  /\  ( x  e.  _V  /\  y  e.  _V ) ) )
30:29:  |-  ( E. y z  =  <. x ,. y >.  <->  E. y ( z  =  <. x ,  y >.  /\  ( x  e.  _V  /\  y  e.  _V ) ) )
31:30:  |-  ( E. x E. y z  =  <. x ,. y >.  <->  E. x  E. y ( z  =  <. x ,  y >.  /\  ( x  e.  _V  /\  y  e.  _V ) ) )
32:31:  |-  { z  |  E. x E. y z  =  <. x ,. y >. }  =  {  z  |  E. x E. y ( z  =  <. x ,  y >.  /\  ( x  e.  _V  /\  y  e.  _V ) ) }
320:25,32:  |-  { z  |  E. x E. y ( z  =  <. x ,. y >.  /\  ( x  e.  _V  /\  y  e.  _V ) ) }  C_  { z  |  E. u E. v z  =  <. u ,  v >. }
33::  |-  u  e.  _V
34::  |-  v  e.  _V
35:33,34:  |-  ( u  e.  _V  /\  v  e.  _V )
36:35:  |-  ( z  =  <. u ,. v >.  <->  ( z  =  <. u ,. v  >.  /\  ( u  e.  _V  /\  v  e.  _V ) ) )
37:36:  |-  ( E. v z  =  <. u ,. v >.  <->  E. v ( z  =  <. u ,  v >.  /\  ( u  e.  _V  /\  v  e.  _V ) ) )
38:37:  |-  ( E. u E. v z  =  <. u ,. v >.  <->  E. u  E. v ( z  =  <. u ,  v >.  /\  ( u  e.  _V  /\  v  e.  _V ) ) )
39:38:  |-  { z  |  E. u E. v z  =  <. u ,. v >. }  =  {  z  |  E. u E. v ( z  =  <. u ,  v >.  /\  ( u  e.  _V  /\  v  e.  _V ) ) }
40:320,39:  |-  { z  |  E. x E. y ( z  =  <. x ,. y >.  /\  ( x  e.  _V  /\  y  e.  _V ) ) }  C_  { z  |  E. u E. v ( z  =  <. u ,  v >.  /\  ( u  e.  _V  /\  v  e.  _V ) ) }
41::  |-  { <. x ,. y >.  |  ( x  e.  _V  /\  y  e.  _V  ) }  =  { z  |  E. x E. y ( z  =  <. x ,  y >.  /\  ( x  e.  _V  /\  y  e.  _V ) )  }
42::  |-  { <. u ,. v >.  |  ( u  e.  _V  /\  v  e.  _V  ) }  =  { z  |  E. u E. v ( z  =  <. u ,  v >.  /\  ( u  e.  _V  /\  v  e.  _V ) )  }
43:40,41,42:  |-  { <. x ,. y >.  |  ( x  e.  _V  /\  y  e.  _V  ) }  C_  { <. u ,  v >.  |  ( u  e.  _V  /\  v  e.  _V ) }
44::  |-  { <. u ,. v >.  |  ( u  e.  _V  /\  v  e.  _V  ) }  =  ( _V  X.  _V )
45:43,44:  |-  { <. x ,. y >.  |  ( x  e.  _V  /\  y  e.  _V  ) }  C_  ( _V  X.  _V )
46:28:  |-  ( ph  ->  ( x  e.  _V  /\  y  e.  _V ) )
47:46:  |-  { <. x ,. y >.  |  ph }  C_  { <. x ,. y >.  |  ( x  e.  _V  /\  y  e.  _V ) }
48:45,47:  |-  { <. x ,. y >.  |  ph }  C_  ( _V  X.  _V )
qed:48:  |-  Rel  { <. x ,. y >.  |  ph }
(Contributed by Alan Sare, 9-Jul-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
relopabVD  |-  Rel  { <. x ,  y >.  |  ph }

Proof of Theorem relopabVD
Dummy variables  z 
v  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3016 . . . . . 6  |-  x  e. 
_V
2 vex 3016 . . . . . 6  |-  y  e. 
_V
31, 2pm3.2i 461 . . . . 5  |-  ( x  e.  _V  /\  y  e.  _V )
43a1i 11 . . . 4  |-  ( ph  ->  ( x  e.  _V  /\  y  e.  _V )
)
54ssopab2i 4702 . . 3  |-  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ( x  e.  _V  /\  y  e.  _V ) }
63biantru 512 . . . . . . . . . 10  |-  ( z  =  <. x ,  y
>. 
<->  ( z  =  <. x ,  y >.  /\  (
x  e.  _V  /\  y  e.  _V )
) )
76exbii 1722 . . . . . . . . 9  |-  ( E. y  z  =  <. x ,  y >.  <->  E. y
( z  =  <. x ,  y >.  /\  (
x  e.  _V  /\  y  e.  _V )
) )
87exbii 1722 . . . . . . . 8  |-  ( E. x E. y  z  =  <. x ,  y
>. 
<->  E. x E. y
( z  =  <. x ,  y >.  /\  (
x  e.  _V  /\  y  e.  _V )
) )
98abbii 2568 . . . . . . 7  |-  { z  |  E. x E. y  z  =  <. x ,  y >. }  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ( x  e. 
_V  /\  y  e.  _V ) ) }
10 ax6ev 1811 . . . . . . . . . . . . . . 15  |-  E. u  u  =  x
11 equcom 1866 . . . . . . . . . . . . . . . 16  |-  ( u  =  x  <->  x  =  u )
1211exbii 1722 . . . . . . . . . . . . . . 15  |-  ( E. u  u  =  x  <->  E. u  x  =  u )
1310, 12mpbi 213 . . . . . . . . . . . . . 14  |-  E. u  x  =  u
14 ax6ev 1811 . . . . . . . . . . . . . . . . . . 19  |-  E. v 
v  =  y
15 equcom 1866 . . . . . . . . . . . . . . . . . . . 20  |-  ( v  =  y  <->  y  =  v )
1615exbii 1722 . . . . . . . . . . . . . . . . . . 19  |-  ( E. v  v  =  y  <->  E. v  y  =  v )
1714, 16mpbi 213 . . . . . . . . . . . . . . . . . 18  |-  E. v 
y  =  v
18 idn1 36944 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (. y  =  v  ->.  y  =  v ).
19 opeq2 4137 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  v  ->  <. x ,  y >.  =  <. x ,  v >. )
2018, 19e1a 37006 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (. y  =  v  ->.  <. x ,  y
>.  =  <. x ,  v >. ).
21 idn2 36992 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (. y  =  v ,. x  =  u  ->.  x  =  u ).
22 opeq1 4136 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  u  ->  <. x ,  v >.  =  <. u ,  v >. )
2321, 22e2 37010 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (. y  =  v ,. x  =  u  ->.  <. x ,  v
>.  =  <. u ,  v >. ).
24 eqeq1 2456 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
x ,  y >.  =  <. x ,  v
>.  ->  ( <. x ,  y >.  =  <. u ,  v >.  <->  <. x ,  v >.  =  <. u ,  v >. )
)
2524biimprd 231 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( <.
x ,  y >.  =  <. x ,  v
>.  ->  ( <. x ,  v >.  =  <. u ,  v >.  ->  <. x ,  y >.  =  <. u ,  v >. )
)
2620, 23, 25e12 37108 . . . . . . . . . . . . . . . . . . . . . 22  |-  (. y  =  v ,. x  =  u  ->.  <. x ,  y
>.  =  <. u ,  v >. ).
27 eqeq2 2463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( <.
x ,  y >.  =  <. u ,  v
>.  ->  ( z  = 
<. x ,  y >.  <->  z  =  <. u ,  v
>. ) )
2827biimpd 212 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( <.
x ,  y >.  =  <. u ,  v
>.  ->  ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. )
)
2926, 28e2 37010 . . . . . . . . . . . . . . . . . . . . 21  |-  (. y  =  v ,. x  =  u  ->.  ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. ) ).
3029in2 36984 . . . . . . . . . . . . . . . . . . . 20  |-  (. y  =  v  ->.  ( x  =  u  ->  ( z  =  <. x ,  y
>.  ->  z  =  <. u ,  v >. )
) ).
3130in1 36941 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  v  ->  (
x  =  u  -> 
( z  =  <. x ,  y >.  ->  z  =  <. u ,  v
>. ) ) )
3231eximi 1711 . . . . . . . . . . . . . . . . . 18  |-  ( E. v  y  =  v  ->  E. v ( x  =  u  ->  (
z  =  <. x ,  y >.  ->  z  =  <. u ,  v
>. ) ) )
3317, 32ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  E. v
( x  =  u  ->  ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. )
)
343319.37iv 1831 . . . . . . . . . . . . . . . 16  |-  ( x  =  u  ->  E. v
( z  =  <. x ,  y >.  ->  z  =  <. u ,  v
>. ) )
35 19.37v 1830 . . . . . . . . . . . . . . . . 17  |-  ( E. v ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. )  <->  ( z  =  <. x ,  y >.  ->  E. v 
z  =  <. u ,  v >. )
)
3635biimpi 199 . . . . . . . . . . . . . . . 16  |-  ( E. v ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. )  ->  ( z  =  <. x ,  y >.  ->  E. v 
z  =  <. u ,  v >. )
)
3734, 36syl 17 . . . . . . . . . . . . . . 15  |-  ( x  =  u  ->  (
z  =  <. x ,  y >.  ->  E. v 
z  =  <. u ,  v >. )
)
3837eximi 1711 . . . . . . . . . . . . . 14  |-  ( E. u  x  =  u  ->  E. u ( z  =  <. x ,  y
>.  ->  E. v  z  = 
<. u ,  v >.
) )
3913, 38ax-mp 5 . . . . . . . . . . . . 13  |-  E. u
( z  =  <. x ,  y >.  ->  E. v 
z  =  <. u ,  v >. )
403919.37iv 1831 . . . . . . . . . . . 12  |-  ( z  =  <. x ,  y
>.  ->  E. u E. v 
z  =  <. u ,  v >. )
4140eximi 1711 . . . . . . . . . . 11  |-  ( E. y  z  =  <. x ,  y >.  ->  E. y E. u E. v  z  =  <. u ,  v
>. )
42 19.9v 1816 . . . . . . . . . . . 12  |-  ( E. y E. u E. v  z  =  <. u ,  v >.  <->  E. u E. v  z  =  <. u ,  v >.
)
4342biimpi 199 . . . . . . . . . . 11  |-  ( E. y E. u E. v  z  =  <. u ,  v >.  ->  E. u E. v  z  =  <. u ,  v >.
)
4441, 43syl 17 . . . . . . . . . 10  |-  ( E. y  z  =  <. x ,  y >.  ->  E. u E. v  z  =  <. u ,  v >.
)
4544eximi 1711 . . . . . . . . 9  |-  ( E. x E. y  z  =  <. x ,  y
>.  ->  E. x E. u E. v  z  =  <. u ,  v >.
)
46 19.9v 1816 . . . . . . . . . 10  |-  ( E. x E. u E. v  z  =  <. u ,  v >.  <->  E. u E. v  z  =  <. u ,  v >.
)
4746biimpi 199 . . . . . . . . 9  |-  ( E. x E. u E. v  z  =  <. u ,  v >.  ->  E. u E. v  z  =  <. u ,  v >.
)
4845, 47syl 17 . . . . . . . 8  |-  ( E. x E. y  z  =  <. x ,  y
>.  ->  E. u E. v 
z  =  <. u ,  v >. )
4948ss2abi 3469 . . . . . . 7  |-  { z  |  E. x E. y  z  =  <. x ,  y >. }  C_  { z  |  E. u E. v  z  =  <. u ,  v >. }
509, 49eqsstr3i 3431 . . . . . 6  |-  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ( x  e.  _V  /\  y  e.  _V )
) }  C_  { z  |  E. u E. v  z  =  <. u ,  v >. }
51 vex 3016 . . . . . . . . . . 11  |-  u  e. 
_V
52 vex 3016 . . . . . . . . . . 11  |-  v  e. 
_V
5351, 52pm3.2i 461 . . . . . . . . . 10  |-  ( u  e.  _V  /\  v  e.  _V )
5453biantru 512 . . . . . . . . 9  |-  ( z  =  <. u ,  v
>. 
<->  ( z  =  <. u ,  v >.  /\  (
u  e.  _V  /\  v  e.  _V )
) )
5554exbii 1722 . . . . . . . 8  |-  ( E. v  z  =  <. u ,  v >.  <->  E. v
( z  =  <. u ,  v >.  /\  (
u  e.  _V  /\  v  e.  _V )
) )
5655exbii 1722 . . . . . . 7  |-  ( E. u E. v  z  =  <. u ,  v
>. 
<->  E. u E. v
( z  =  <. u ,  v >.  /\  (
u  e.  _V  /\  v  e.  _V )
) )
5756abbii 2568 . . . . . 6  |-  { z  |  E. u E. v  z  =  <. u ,  v >. }  =  { z  |  E. u E. v ( z  =  <. u ,  v
>.  /\  ( u  e. 
_V  /\  v  e.  _V ) ) }
5850, 57sseqtri 3432 . . . . 5  |-  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ( x  e.  _V  /\  y  e.  _V )
) }  C_  { z  |  E. u E. v ( z  = 
<. u ,  v >.  /\  ( u  e.  _V  /\  v  e.  _V )
) }
59 df-opab 4434 . . . . 5  |-  { <. x ,  y >.  |  ( x  e.  _V  /\  y  e.  _V ) }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  (
x  e.  _V  /\  y  e.  _V )
) }
60 df-opab 4434 . . . . 5  |-  { <. u ,  v >.  |  ( u  e.  _V  /\  v  e.  _V ) }  =  { z  |  E. u E. v
( z  =  <. u ,  v >.  /\  (
u  e.  _V  /\  v  e.  _V )
) }
6158, 59, 603sstr4i 3439 . . . 4  |-  { <. x ,  y >.  |  ( x  e.  _V  /\  y  e.  _V ) }  C_  { <. u ,  v >.  |  ( u  e.  _V  /\  v  e.  _V ) }
62 df-xp 4818 . . . . 5  |-  ( _V 
X.  _V )  =  { <. u ,  v >.  |  ( u  e. 
_V  /\  v  e.  _V ) }
6362eqcomi 2461 . . . 4  |-  { <. u ,  v >.  |  ( u  e.  _V  /\  v  e.  _V ) }  =  ( _V  X.  _V )
6461, 63sseqtri 3432 . . 3  |-  { <. x ,  y >.  |  ( x  e.  _V  /\  y  e.  _V ) }  C_  ( _V  X.  _V )
655, 64sstri 3409 . 2  |-  { <. x ,  y >.  |  ph }  C_  ( _V  X.  _V )
66 df-rel 4819 . . 3  |-  ( Rel 
{ <. x ,  y
>.  |  ph }  <->  { <. x ,  y >.  |  ph }  C_  ( _V  X.  _V ) )
6766biimpri 211 . 2  |-  ( {
<. x ,  y >.  |  ph }  C_  ( _V  X.  _V )  ->  Rel  { <. x ,  y
>.  |  ph } )
6865, 67e0a 37156 1  |-  Rel  { <. x ,  y >.  |  ph }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1448   E.wex 1667    e. wcel 1891   {cab 2438   _Vcvv 3013    C_ wss 3372   <.cop 3942   {copab 4432    X. cxp 4810   Rel wrel 4817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-rab 2746  df-v 3015  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-opab 4434  df-xp 4818  df-rel 4819  df-vd1 36940  df-vd2 36948
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator