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 .

		Ref	Expression
	Assertion	relopabVD	$⊢ Rel \{⟨x, y⟩ \| φ\}$

Proof

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

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 }

Metamath Proof Explorer

Theorem relopabVD

Proof