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 .

	Ref	Expression
Assertion	relopabVD	$$⊢\mathrm{Rel}\left\{⟨x,y⟩|\phi \right\}$$

Proof

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