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

Theorem relopabVD 28677
Description: Virtual deduction proof of relopab 4812. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. relopab 4812 is relopabVD 28677 without virtual deductions and was automatically derived from relopabVD 28677.
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 2791 . . . . . 6  |-  x  e. 
_V
2 vex 2791 . . . . . 6  |-  y  e. 
_V
31, 2pm3.2i 441 . . . . 5  |-  ( x  e.  _V  /\  y  e.  _V )
43a1i 10 . . . 4  |-  ( ph  ->  ( x  e.  _V  /\  y  e.  _V )
)
54ssopab2i 4292 . . 3  |-  { <. x ,  y >.  |  ph }  C_  { <. x ,  y >.  |  ( x  e.  _V  /\  y  e.  _V ) }
63biantru 491 . . . . . . . . . 10  |-  ( z  =  <. x ,  y
>. 
<->  ( z  =  <. x ,  y >.  /\  (
x  e.  _V  /\  y  e.  _V )
) )
76exbii 1569 . . . . . . . . 9  |-  ( E. y  z  =  <. x ,  y >.  <->  E. y
( z  =  <. x ,  y >.  /\  (
x  e.  _V  /\  y  e.  _V )
) )
87exbii 1569 . . . . . . . 8  |-  ( E. x E. y  z  =  <. x ,  y
>. 
<->  E. x E. y
( z  =  <. x ,  y >.  /\  (
x  e.  _V  /\  y  e.  _V )
) )
98abbii 2395 . . . . . . 7  |-  { z  |  E. x E. y  z  =  <. x ,  y >. }  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ( x  e. 
_V  /\  y  e.  _V ) ) }
10 a9ev 1637 . . . . . . . . . . . . . . 15  |-  E. u  u  =  x
11 equcom 1647 . . . . . . . . . . . . . . . 16  |-  ( u  =  x  <->  x  =  u )
1211exbii 1569 . . . . . . . . . . . . . . 15  |-  ( E. u  u  =  x  <->  E. u  x  =  u )
1310, 12mpbi 199 . . . . . . . . . . . . . 14  |-  E. u  x  =  u
14 a9ev 1637 . . . . . . . . . . . . . . . . . . 19  |-  E. v 
v  =  y
15 equcom 1647 . . . . . . . . . . . . . . . . . . . 20  |-  ( v  =  y  <->  y  =  v )
1615exbii 1569 . . . . . . . . . . . . . . . . . . 19  |-  ( E. v  v  =  y  <->  E. v  y  =  v )
1714, 16mpbi 199 . . . . . . . . . . . . . . . . . 18  |-  E. v 
y  =  v
18 idn1 28342 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (. y  =  v  ->.  y  =  v ).
19 opeq2 3797 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  v  ->  <. x ,  y >.  =  <. x ,  v >. )
2018, 19e1_ 28399 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (. y  =  v  ->.  <. x ,  y
>.  =  <. x ,  v >. ).
21 idn2 28385 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (. y  =  v ,. x  =  u  ->.  x  =  u ).
22 opeq1 3796 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  u  ->  <. x ,  v >.  =  <. u ,  v >. )
2321, 22e2 28403 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (. y  =  v ,. x  =  u  ->.  <. x ,  v
>.  =  <. u ,  v >. ).
24 eqeq1 2289 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
x ,  y >.  =  <. x ,  v
>.  ->  ( <. x ,  y >.  =  <. u ,  v >.  <->  <. x ,  v >.  =  <. u ,  v >. )
)
2524biimprd 214 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( <.
x ,  y >.  =  <. x ,  v
>.  ->  ( <. x ,  v >.  =  <. u ,  v >.  ->  <. x ,  y >.  =  <. u ,  v >. )
)
2620, 23, 25e12 28499 . . . . . . . . . . . . . . . . . . . . . 22  |-  (. y  =  v ,. x  =  u  ->.  <. x ,  y
>.  =  <. u ,  v >. ).
27 eqeq2 2292 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( <.
x ,  y >.  =  <. u ,  v
>.  ->  ( z  = 
<. x ,  y >.  <->  z  =  <. u ,  v
>. ) )
2827biimpd 198 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( <.
x ,  y >.  =  <. u ,  v
>.  ->  ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. )
)
2926, 28e2 28403 . . . . . . . . . . . . . . . . . . . . 21  |-  (. y  =  v ,. x  =  u  ->.  ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. ) ).
3029in2 28377 . . . . . . . . . . . . . . . . . . . 20  |-  (. y  =  v  ->.  ( x  =  u  ->  ( z  =  <. x ,  y
>.  ->  z  =  <. u ,  v >. )
) ).
3130in1 28339 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  v  ->  (
x  =  u  -> 
( z  =  <. x ,  y >.  ->  z  =  <. u ,  v
>. ) ) )
3231eximi 1563 . . . . . . . . . . . . . . . . . 18  |-  ( E. v  y  =  v  ->  E. v ( x  =  u  ->  (
z  =  <. x ,  y >.  ->  z  =  <. u ,  v
>. ) ) )
3317, 32ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  E. v
( x  =  u  ->  ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. )
)
343319.37aiv 1841 . . . . . . . . . . . . . . . 16  |-  ( x  =  u  ->  E. v
( z  =  <. x ,  y >.  ->  z  =  <. u ,  v
>. ) )
35 19.37v 1840 . . . . . . . . . . . . . . . . 17  |-  ( E. v ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. )  <->  ( z  =  <. x ,  y >.  ->  E. v 
z  =  <. u ,  v >. )
)
3635biimpi 186 . . . . . . . . . . . . . . . 16  |-  ( E. v ( z  = 
<. x ,  y >.  ->  z  =  <. u ,  v >. )  ->  ( z  =  <. x ,  y >.  ->  E. v 
z  =  <. u ,  v >. )
)
3734, 36syl 15 . . . . . . . . . . . . . . 15  |-  ( x  =  u  ->  (
z  =  <. x ,  y >.  ->  E. v 
z  =  <. u ,  v >. )
)
3837eximi 1563 . . . . . . . . . . . . . 14  |-  ( E. u  x  =  u  ->  E. u ( z  =  <. x ,  y
>.  ->  E. v  z  = 
<. u ,  v >.
) )
3913, 38ax-mp 8 . . . . . . . . . . . . 13  |-  E. u
( z  =  <. x ,  y >.  ->  E. v 
z  =  <. u ,  v >. )
403919.37aiv 1841 . . . . . . . . . . . 12  |-  ( z  =  <. x ,  y
>.  ->  E. u E. v 
z  =  <. u ,  v >. )
4140eximi 1563 . . . . . . . . . . 11  |-  ( E. y  z  =  <. x ,  y >.  ->  E. y E. u E. v  z  =  <. u ,  v
>. )
42 19.9v 1663 . . . . . . . . . . . 12  |-  ( E. y E. u E. v  z  =  <. u ,  v >.  <->  E. u E. v  z  =  <. u ,  v >.
)
4342biimpi 186 . . . . . . . . . . 11  |-  ( E. y E. u E. v  z  =  <. u ,  v >.  ->  E. u E. v  z  =  <. u ,  v >.
)
4441, 43syl 15 . . . . . . . . . 10  |-  ( E. y  z  =  <. x ,  y >.  ->  E. u E. v  z  =  <. u ,  v >.
)
4544eximi 1563 . . . . . . . . 9  |-  ( E. x E. y  z  =  <. x ,  y
>.  ->  E. x E. u E. v  z  =  <. u ,  v >.
)
46 19.9v 1663 . . . . . . . . . 10  |-  ( E. x E. u E. v  z  =  <. u ,  v >.  <->  E. u E. v  z  =  <. u ,  v >.
)
4746biimpi 186 . . . . . . . . 9  |-  ( E. x E. u E. v  z  =  <. u ,  v >.  ->  E. u E. v  z  =  <. u ,  v >.
)
4845, 47syl 15 . . . . . . . 8  |-  ( E. x E. y  z  =  <. x ,  y
>.  ->  E. u E. v 
z  =  <. u ,  v >. )
4948ss2abi 3245 . . . . . . 7  |-  { z  |  E. x E. y  z  =  <. x ,  y >. }  C_  { z  |  E. u E. v  z  =  <. u ,  v >. }
509, 49eqsstr3i 3209 . . . . . 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 2791 . . . . . . . . . . 11  |-  u  e. 
_V
52 vex 2791 . . . . . . . . . . 11  |-  v  e. 
_V
5351, 52pm3.2i 441 . . . . . . . . . 10  |-  ( u  e.  _V  /\  v  e.  _V )
5453biantru 491 . . . . . . . . 9  |-  ( z  =  <. u ,  v
>. 
<->  ( z  =  <. u ,  v >.  /\  (
u  e.  _V  /\  v  e.  _V )
) )
5554exbii 1569 . . . . . . . 8  |-  ( E. v  z  =  <. u ,  v >.  <->  E. v
( z  =  <. u ,  v >.  /\  (
u  e.  _V  /\  v  e.  _V )
) )
5655exbii 1569 . . . . . . 7  |-  ( E. u E. v  z  =  <. u ,  v
>. 
<->  E. u E. v
( z  =  <. u ,  v >.  /\  (
u  e.  _V  /\  v  e.  _V )
) )
5756abbii 2395 . . . . . 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 3210 . . . . 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 4078 . . . . 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 4078 . . . . 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 3217 . . . 4  |-  { <. x ,  y >.  |  ( x  e.  _V  /\  y  e.  _V ) }  C_  { <. u ,  v >.  |  ( u  e.  _V  /\  v  e.  _V ) }
62 df-xp 4695 . . . . 5  |-  ( _V 
X.  _V )  =  { <. u ,  v >.  |  ( u  e. 
_V  /\  v  e.  _V ) }
6362eqcomi 2287 . . . 4  |-  { <. u ,  v >.  |  ( u  e.  _V  /\  v  e.  _V ) }  =  ( _V  X.  _V )
6461, 63sseqtri 3210 . . 3  |-  { <. x ,  y >.  |  ( x  e.  _V  /\  y  e.  _V ) }  C_  ( _V  X.  _V )
655, 64sstri 3188 . 2  |-  { <. x ,  y >.  |  ph }  C_  ( _V  X.  _V )
66 df-rel 4696 . . 3  |-  ( Rel 
{ <. x ,  y
>.  |  ph }  <->  { <. x ,  y >.  |  ph }  C_  ( _V  X.  _V ) )
6766biimpri 197 . 2  |-  ( {
<. x ,  y >.  |  ph }  C_  ( _V  X.  _V )  ->  Rel  { <. x ,  y
>.  |  ph } )
6865, 67e0_ 28547 1  |-  Rel  { <. x ,  y >.  |  ph }
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1528    = wceq 1623    e. wcel 1684   {cab 2269   _Vcvv 2788    C_ wss 3152   <.cop 3643   {copab 4076    X. cxp 4687   Rel wrel 4694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-xp 4695  df-rel 4696  df-vd1 28338  df-vd2 28347
  Copyright terms: Public domain W3C validator