Theorem relopabi

Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021)

	Ref	Expression
Hypothesis	relopabi.1	$$⊢A=\left\{⟨x,y⟩|\phi \right\}$$
Assertion	relopabi	$$⊢\mathrm{Rel}A$$

Proof

Step	Hyp	Ref	Expression
1		relopabi.1	$$⊢A=\left\{⟨x,y⟩|\phi \right\}$$
2		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}$$
3	1 2	eqtri	$$⊢A=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}$$
4	3	abeq2i	$$⊢z\in A\leftrightarrow \exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)$$
5		simpl	$$⊢\left(z=⟨x,y⟩\wedge \phi \right)\to z=⟨x,y⟩$$
6	5	2eximi	$$⊢\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\to \exists x\exists yz=⟨x,y⟩$$
7	4 6	sylbi	$$⊢z\in A\to \exists x\exists yz=⟨x,y⟩$$
8		ax6evr	$$⊢\exists uy=u$$
9		pm3.21	$$⊢⟨x,y⟩=z\to \left(y=u\to \left(y=u\wedge ⟨x,y⟩=z\right)\right)$$
10	9	eximdv	$$⊢⟨x,y⟩=z\to \left(\exists uy=u\to \exists u\left(y=u\wedge ⟨x,y⟩=z\right)\right)$$
11	8 10	mpi	$$⊢⟨x,y⟩=z\to \exists u\left(y=u\wedge ⟨x,y⟩=z\right)$$
12		opeq2	$$⊢y=u\to ⟨x,y⟩=⟨x,u⟩$$
13		eqtr2	$$⊢\left(⟨x,y⟩=⟨x,u⟩\wedge ⟨x,y⟩=z\right)\to ⟨x,u⟩=z$$
14	13	eqcomd	$$⊢\left(⟨x,y⟩=⟨x,u⟩\wedge ⟨x,y⟩=z\right)\to z=⟨x,u⟩$$
15	12 14	sylan	$$⊢\left(y=u\wedge ⟨x,y⟩=z\right)\to z=⟨x,u⟩$$
16	15	eximi	$$⊢\exists u\left(y=u\wedge ⟨x,y⟩=z\right)\to \exists uz=⟨x,u⟩$$
17	11 16	syl	$$⊢⟨x,y⟩=z\to \exists uz=⟨x,u⟩$$
18	17	eqcoms	$$⊢z=⟨x,y⟩\to \exists uz=⟨x,u⟩$$
19	18	2eximi	$$⊢\exists x\exists yz=⟨x,y⟩\to \exists x\exists y\exists uz=⟨x,u⟩$$
20		excomim	$$⊢\exists x\exists y\exists uz=⟨x,u⟩\to \exists y\exists x\exists uz=⟨x,u⟩$$
21	19 20	syl	$$⊢\exists x\exists yz=⟨x,y⟩\to \exists y\exists x\exists uz=⟨x,u⟩$$
22		vex	$$⊢x\in \mathrm{V}$$
23		vex	$$⊢u\in \mathrm{V}$$
24	22 23	pm3.2i	$$⊢\left(x\in \mathrm{V}\wedge u\in \mathrm{V}\right)$$
25	24	jctr	$$⊢z=⟨x,u⟩\to \left(z=⟨x,u⟩\wedge \left(x\in \mathrm{V}\wedge u\in \mathrm{V}\right)\right)$$
26	25	2eximi	$$⊢\exists x\exists uz=⟨x,u⟩\to \exists x\exists u\left(z=⟨x,u⟩\wedge \left(x\in \mathrm{V}\wedge u\in \mathrm{V}\right)\right)$$
27		df-xp	$$⊢\mathrm{V}\times \mathrm{V}=\left\{⟨x,u⟩|\left(x\in \mathrm{V}\wedge u\in \mathrm{V}\right)\right\}$$
28		df-opab	$$⊢\left\{⟨x,u⟩|\left(x\in \mathrm{V}\wedge u\in \mathrm{V}\right)\right\}=\left\{z|\exists x\exists u\left(z=⟨x,u⟩\wedge \left(x\in \mathrm{V}\wedge u\in \mathrm{V}\right)\right)\right\}$$
29	27 28	eqtri	$$⊢\mathrm{V}\times \mathrm{V}=\left\{z|\exists x\exists u\left(z=⟨x,u⟩\wedge \left(x\in \mathrm{V}\wedge u\in \mathrm{V}\right)\right)\right\}$$
30	29	abeq2i	$$⊢z\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\exists u\left(z=⟨x,u⟩\wedge \left(x\in \mathrm{V}\wedge u\in \mathrm{V}\right)\right)$$
31	26 30	sylibr	$$⊢\exists x\exists uz=⟨x,u⟩\to z\in \left(\mathrm{V}\times \mathrm{V}\right)$$
32	31	eximi	$$⊢\exists y\exists x\exists uz=⟨x,u⟩\to \exists yz\in \left(\mathrm{V}\times \mathrm{V}\right)$$
33	7 21 32	3syl	$$⊢z\in A\to \exists yz\in \left(\mathrm{V}\times \mathrm{V}\right)$$
34		ax5e	$$⊢\exists yz\in \left(\mathrm{V}\times \mathrm{V}\right)\to z\in \left(\mathrm{V}\times \mathrm{V}\right)$$
35	33 34	syl	$$⊢z\in A\to z\in \left(\mathrm{V}\times \mathrm{V}\right)$$
36	35	ssriv	$$⊢A\subseteq \mathrm{V}\times \mathrm{V}$$
37		df-rel	$$⊢\mathrm{Rel}A\leftrightarrow A\subseteq \mathrm{V}\times \mathrm{V}$$
38	36 37	mpbir	$$⊢\mathrm{Rel}A$$