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

Theorem relopabVD 34102
Description: Virtual deduction proof of relopab 5117. 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 5117 is relopabVD 34102 without virtual deductions and was automatically derived from relopabVD 34102.
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 3109 . . . . . 6  |-  x  e. 
_V
2 vex 3109 . . . . . 6  |-  y  e. 
_V
31, 2pm3.2i 453 . . . . 5  |-  ( x  e.  _V  /\  y  e.  _V )
43a1i 11 . . . 4  |-  ( ph  ->  ( x  e.  _V  /\  y  e.  _V )
)
54ssopab2i 4764 . . 3  |-  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ( x  e.  _V  /\  y  e.  _V ) }
63biantru 503 . . . . . . . . . 10  |-  ( z  =  <. x ,  y
>. 
<->  ( z  =  <. x ,  y >.  /\  (
x  e.  _V  /\  y  e.  _V )
) )
76exbii 1672 . . . . . . . . 9  |-  ( E. y  z  =  <. x ,  y >.  <->  E. y
( z  =  <. x ,  y >.  /\  (
x  e.  _V  /\  y  e.  _V )
) )
87exbii 1672 . . . . . . . 8  |-  ( E. x E. y  z  =  <. x ,  y
>. 
<->  E. x E. y
( z  =  <. x ,  y >.  /\  (
x  e.  _V  /\  y  e.  _V )
) )
98abbii 2588 . . . . . . 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 1754 . . . . . . . . . . . . . . 15  |-  E. u  u  =  x
11 equcom 1799 . . . . . . . . . . . . . . . 16  |-  ( u  =  x  <->  x  =  u )
1211exbii 1672 . . . . . . . . . . . . . . 15  |-  ( E. u  u  =  x  <->  E. u  x  =  u )
1310, 12mpbi 208 . . . . . . . . . . . . . 14  |-  E. u  x  =  u
14 ax6ev 1754 . . . . . . . . . . . . . . . . . . 19  |-  E. v 
v  =  y
15 equcom 1799 . . . . . . . . . . . . . . . . . . . 20  |-  ( v  =  y  <->  y  =  v )
1615exbii 1672 . . . . . . . . . . . . . . . . . . 19  |-  ( E. v  v  =  y  <->  E. v  y  =  v )
1714, 16mpbi 208 . . . . . . . . . . . . . . . . . 18  |-  E. v 
y  =  v
18 idn1 33745 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (. y  =  v  ->.  y  =  v ).
19 opeq2 4204 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  v  ->  <. x ,  y >.  =  <. x ,  v >. )
2018, 19e1a 33807 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (. y  =  v  ->.  <. x ,  y
>.  =  <. x ,  v >. ).
21 idn2 33793 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (. y  =  v ,. x  =  u  ->.  x  =  u ).
22 opeq1 4203 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  u  ->  <. x ,  v >.  =  <. u ,  v >. )
2321, 22e2 33811 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (. y  =  v ,. x  =  u  ->.  <. x ,  v
>.  =  <. u ,  v >. ).
24 eqeq1 2458 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
x ,  y >.  =  <. x ,  v
>.  ->  ( <. x ,  y >.  =  <. u ,  v >.  <->  <. x ,  v >.  =  <. u ,  v >. )
)
2524biimprd 223 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( <.
x ,  y >.  =  <. x ,  v
>.  ->  ( <. x ,  v >.  =  <. u ,  v >.  ->  <. x ,  y >.  =  <. u ,  v >. )
)
2620, 23, 25e12 33915 . . . . . . . . . . . . . . . . . . . . . 22  |-  (. y  =  v ,. x  =  u  ->.  <. x ,  y
>.  =  <. u ,  v >. ).
27 eqeq2 2469 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( <.
x ,  y >.  =  <. u ,  v
>.  ->  ( z  = 
<. x ,  y >.  <->  z  =  <. u ,  v
>. ) )
2827biimpd 207 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( <.
x ,  y >.  =  <. u ,  v
>.  ->  ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. )
)
2926, 28e2 33811 . . . . . . . . . . . . . . . . . . . . 21  |-  (. y  =  v ,. x  =  u  ->.  ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. ) ).
3029in2 33785 . . . . . . . . . . . . . . . . . . . 20  |-  (. y  =  v  ->.  ( x  =  u  ->  ( z  =  <. x ,  y
>.  ->  z  =  <. u ,  v >. )
) ).
3130in1 33742 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  v  ->  (
x  =  u  -> 
( z  =  <. x ,  y >.  ->  z  =  <. u ,  v
>. ) ) )
3231eximi 1661 . . . . . . . . . . . . . . . . . 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 1774 . . . . . . . . . . . . . . . 16  |-  ( x  =  u  ->  E. v
( z  =  <. x ,  y >.  ->  z  =  <. u ,  v
>. ) )
35 19.37v 1773 . . . . . . . . . . . . . . . . 17  |-  ( E. v ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. )  <->  ( z  =  <. x ,  y >.  ->  E. v 
z  =  <. u ,  v >. )
)
3635biimpi 194 . . . . . . . . . . . . . . . 16  |-  ( E. v ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. )  ->  ( z  =  <. x ,  y >.  ->  E. v 
z  =  <. u ,  v >. )
)
3734, 36syl 16 . . . . . . . . . . . . . . 15  |-  ( x  =  u  ->  (
z  =  <. x ,  y >.  ->  E. v 
z  =  <. u ,  v >. )
)
3837eximi 1661 . . . . . . . . . . . . . 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 1774 . . . . . . . . . . . 12  |-  ( z  =  <. x ,  y
>.  ->  E. u E. v 
z  =  <. u ,  v >. )
4140eximi 1661 . . . . . . . . . . 11  |-  ( E. y  z  =  <. x ,  y >.  ->  E. y E. u E. v  z  =  <. u ,  v
>. )
42 19.9v 1759 . . . . . . . . . . . 12  |-  ( E. y E. u E. v  z  =  <. u ,  v >.  <->  E. u E. v  z  =  <. u ,  v >.
)
4342biimpi 194 . . . . . . . . . . 11  |-  ( E. y E. u E. v  z  =  <. u ,  v >.  ->  E. u E. v  z  =  <. u ,  v >.
)
4441, 43syl 16 . . . . . . . . . 10  |-  ( E. y  z  =  <. x ,  y >.  ->  E. u E. v  z  =  <. u ,  v >.
)
4544eximi 1661 . . . . . . . . 9  |-  ( E. x E. y  z  =  <. x ,  y
>.  ->  E. x E. u E. v  z  =  <. u ,  v >.
)
46 19.9v 1759 . . . . . . . . . 10  |-  ( E. x E. u E. v  z  =  <. u ,  v >.  <->  E. u E. v  z  =  <. u ,  v >.
)
4746biimpi 194 . . . . . . . . 9  |-  ( E. x E. u E. v  z  =  <. u ,  v >.  ->  E. u E. v  z  =  <. u ,  v >.
)
4845, 47syl 16 . . . . . . . 8  |-  ( E. x E. y  z  =  <. x ,  y
>.  ->  E. u E. v 
z  =  <. u ,  v >. )
4948ss2abi 3558 . . . . . . 7  |-  { z  |  E. x E. y  z  =  <. x ,  y >. }  C_  { z  |  E. u E. v  z  =  <. u ,  v >. }
509, 49eqsstr3i 3520 . . . . . 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 3109 . . . . . . . . . . 11  |-  u  e. 
_V
52 vex 3109 . . . . . . . . . . 11  |-  v  e. 
_V
5351, 52pm3.2i 453 . . . . . . . . . 10  |-  ( u  e.  _V  /\  v  e.  _V )
5453biantru 503 . . . . . . . . 9  |-  ( z  =  <. u ,  v
>. 
<->  ( z  =  <. u ,  v >.  /\  (
u  e.  _V  /\  v  e.  _V )
) )
5554exbii 1672 . . . . . . . 8  |-  ( E. v  z  =  <. u ,  v >.  <->  E. v
( z  =  <. u ,  v >.  /\  (
u  e.  _V  /\  v  e.  _V )
) )
5655exbii 1672 . . . . . . 7  |-  ( E. u E. v  z  =  <. u ,  v
>. 
<->  E. u E. v
( z  =  <. u ,  v >.  /\  (
u  e.  _V  /\  v  e.  _V )
) )
5756abbii 2588 . . . . . 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 3521 . . . . 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 4498 . . . . 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 4498 . . . . 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 3528 . . . 4  |-  { <. x ,  y >.  |  ( x  e.  _V  /\  y  e.  _V ) }  C_  { <. u ,  v >.  |  ( u  e.  _V  /\  v  e.  _V ) }
62 df-xp 4994 . . . . 5  |-  ( _V 
X.  _V )  =  { <. u ,  v >.  |  ( u  e. 
_V  /\  v  e.  _V ) }
6362eqcomi 2467 . . . 4  |-  { <. u ,  v >.  |  ( u  e.  _V  /\  v  e.  _V ) }  =  ( _V  X.  _V )
6461, 63sseqtri 3521 . . 3  |-  { <. x ,  y >.  |  ( x  e.  _V  /\  y  e.  _V ) }  C_  ( _V  X.  _V )
655, 64sstri 3498 . 2  |-  { <. x ,  y >.  |  ph }  C_  ( _V  X.  _V )
66 df-rel 4995 . . 3  |-  ( Rel 
{ <. x ,  y
>.  |  ph }  <->  { <. x ,  y >.  |  ph }  C_  ( _V  X.  _V ) )
6766biimpri 206 . 2  |-  ( {
<. x ,  y >.  |  ph }  C_  ( _V  X.  _V )  ->  Rel  { <. x ,  y
>.  |  ph } )
6865, 67e0a 33963 1  |-  Rel  { <. x ,  y >.  |  ph }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398   E.wex 1617    e. wcel 1823   {cab 2439   _Vcvv 3106    C_ wss 3461   <.cop 4022   {copab 4496    X. cxp 4986   Rel wrel 4993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-opab 4498  df-xp 4994  df-rel 4995  df-vd1 33741  df-vd2 33749
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator