Metamath Proof Explorer

Theorem relopabVD

Description: Virtual deduction proof of relopab . 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 is relopabVD without virtual deductions and was automatically derived from relopabVD .

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.)

Ref Expression
Assertion relopabVD 
|- Rel { <. x , y >. | ph }

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 vex 
 |-  y e. _V
3 1 2 pm3.2i 
 |-  ( x e. _V /\ y e. _V )
4 3 a1i 
 |-  ( ph -> ( x e. _V /\ y e. _V ) )
5 4 ssopab2i 
 |-  { <. x , y >. | ph } C_ { <. x , y >. | ( x e. _V /\ y e. _V ) }
6 3 biantru 
 |-  ( z = <. x , y >. <-> ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
7 6 exbii 
 |-  ( E. y z = <. x , y >. <-> E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
8 7 exbii 
 |-  ( E. x E. y z = <. x , y >. <-> E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
9 8 abbii 
 |-  { z | E. x E. y z = <. x , y >. } = { z | E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) }
10 ax6ev 
 |-  E. u u = x
11 equcom 
 |-  ( u = x <-> x = u )
12 11 exbii 
 |-  ( E. u u = x <-> E. u x = u )
13 10 12 mpbi 
 |-  E. u x = u
14 ax6ev 
 |-  E. v v = y
15 equcom 
 |-  ( v = y <-> y = v )
16 15 exbii 
 |-  ( E. v v = y <-> E. v y = v )
17 14 16 mpbi 
 |-  E. v y = v
18 idn1 
 |-  (. y = v ->. y = v ).
19 opeq2 
 |-  ( y = v -> <. x , y >. = <. x , v >. )
20 18 19 e1a 
 |-  (. y = v ->. <. x , y >. = <. x , v >. ).
21 idn2 
 |-  (. y = v ,. x = u ->. x = u ).
22 opeq1 
 |-  ( x = u -> <. x , v >. = <. u , v >. )
23 21 22 e2 
 |-  (. y = v ,. x = u ->. <. x , v >. = <. u , v >. ).
24 eqeq1 
 |-  ( <. x , y >. = <. x , v >. -> ( <. x , y >. = <. u , v >. <-> <. x , v >. = <. u , v >. ) )
25 24 biimprd 
 |-  ( <. x , y >. = <. x , v >. -> ( <. x , v >. = <. u , v >. -> <. x , y >. = <. u , v >. ) )
26 20 23 25 e12 
 |-  (. y = v ,. x = u ->. <. x , y >. = <. u , v >. ).
27 eqeq2 
 |-  ( <. x , y >. = <. u , v >. -> ( z = <. x , y >. <-> z = <. u , v >. ) )
28 27 biimpd 
 |-  ( <. x , y >. = <. u , v >. -> ( z = <. x , y >. -> z = <. u , v >. ) )
29 26 28 e2 
 |-  (. y = v ,. x = u ->. ( z = <. x , y >. -> z = <. u , v >. ) ).
30 29 in2 
 |-  (. y = v ->. ( x = u -> ( z = <. x , y >. -> z = <. u , v >. ) ) ).
31 30 in1 
 |-  ( y = v -> ( x = u -> ( z = <. x , y >. -> z = <. u , v >. ) ) )
32 31 eximi 
 |-  ( E. v y = v -> E. v ( x = u -> ( z = <. x , y >. -> z = <. u , v >. ) ) )
33 17 32 ax-mp 
 |-  E. v ( x = u -> ( z = <. x , y >. -> z = <. u , v >. ) )
34 33 19.37iv 
 |-  ( x = u -> E. v ( z = <. x , y >. -> z = <. u , v >. ) )
35 19.37v 
 |-  ( E. v ( z = <. x , y >. -> z = <. u , v >. ) <-> ( z = <. x , y >. -> E. v z = <. u , v >. ) )
36 35 biimpi 
 |-  ( E. v ( z = <. x , y >. -> z = <. u , v >. ) -> ( z = <. x , y >. -> E. v z = <. u , v >. ) )
37 34 36 syl 
 |-  ( x = u -> ( z = <. x , y >. -> E. v z = <. u , v >. ) )
38 37 eximi 
 |-  ( E. u x = u -> E. u ( z = <. x , y >. -> E. v z = <. u , v >. ) )
39 13 38 ax-mp 
 |-  E. u ( z = <. x , y >. -> E. v z = <. u , v >. )
40 39 19.37iv 
 |-  ( z = <. x , y >. -> E. u E. v z = <. u , v >. )
41 40 eximi 
 |-  ( E. y z = <. x , y >. -> E. y E. u E. v z = <. u , v >. )
42 19.9v 
 |-  ( E. y E. u E. v z = <. u , v >. <-> E. u E. v z = <. u , v >. )
43 42 biimpi 
 |-  ( E. y E. u E. v z = <. u , v >. -> E. u E. v z = <. u , v >. )
44 41 43 syl 
 |-  ( E. y z = <. x , y >. -> E. u E. v z = <. u , v >. )
45 44 eximi 
 |-  ( E. x E. y z = <. x , y >. -> E. x E. u E. v z = <. u , v >. )
46 19.9v 
 |-  ( E. x E. u E. v z = <. u , v >. <-> E. u E. v z = <. u , v >. )
47 46 biimpi 
 |-  ( E. x E. u E. v z = <. u , v >. -> E. u E. v z = <. u , v >. )
48 45 47 syl 
 |-  ( E. x E. y z = <. x , y >. -> E. u E. v z = <. u , v >. )
49 48 ss2abi 
 |-  { z | E. x E. y z = <. x , y >. } C_ { z | E. u E. v z = <. u , v >. }
50 9 49 eqsstrri 
 |-  { 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 
 |-  u e. _V
52 vex 
 |-  v e. _V
53 51 52 pm3.2i 
 |-  ( u e. _V /\ v e. _V )
54 53 biantru 
 |-  ( z = <. u , v >. <-> ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) )
55 54 exbii 
 |-  ( E. v z = <. u , v >. <-> E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) )
56 55 exbii 
 |-  ( E. u E. v z = <. u , v >. <-> E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) )
57 56 abbii 
 |-  { z | E. u E. v z = <. u , v >. } = { z | E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) }
58 50 57 sseqtri 
 |-  { 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 
 |-  { <. 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 
 |-  { <. u , v >. | ( u e. _V /\ v e. _V ) } = { z | E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) }
61 58 59 60 3sstr4i 
 |-  { <. x , y >. | ( x e. _V /\ y e. _V ) } C_ { <. u , v >. | ( u e. _V /\ v e. _V ) }
62 df-xp 
 |-  ( _V X. _V ) = { <. u , v >. | ( u e. _V /\ v e. _V ) }
63 62 eqcomi 
 |-  { <. u , v >. | ( u e. _V /\ v e. _V ) } = ( _V X. _V )
64 61 63 sseqtri 
 |-  { <. x , y >. | ( x e. _V /\ y e. _V ) } C_ ( _V X. _V )
65 5 64 sstri 
 |-  { <. x , y >. | ph } C_ ( _V X. _V )
66 df-rel 
 |-  ( Rel { <. x , y >. | ph } <-> { <. x , y >. | ph } C_ ( _V X. _V ) )
67 66 biimpri 
 |-  ( { <. x , y >. | ph } C_ ( _V X. _V ) -> Rel { <. x , y >. | ph } )
68 65 67 e0a 
 |-  Rel { <. x , y >. | ph }