relop

Description: A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008) A relation is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a relation is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is relsnopg , as funsng is to funop . (New usage is discouraged.)

	Ref	Expression
Hypotheses	relop.1	$⊢ A \in V$
	relop.2	$⊢ B \in V$
Assertion	relop	$⊢ Rel ⟨A, B⟩ \leftrightarrow \exists x \exists y (A = \{x\} \land B = \{x, y\})$

Proof

Step	Hyp	Ref	Expression
1		relop.1	$⊢ A \in V$
2		relop.2	$⊢ B \in V$
3		df-rel	$⊢ Rel ⟨A, B⟩ \leftrightarrow ⟨A, B⟩ \subseteq V \times V$
4		dfss2	$⊢ ⟨A, B⟩ \subseteq V \times V \leftrightarrow \forall z (z \in ⟨A, B⟩ \to z \in (V \times V))$
5	1 2	elop	$⊢ z \in ⟨A, B⟩ \leftrightarrow (z = \{A\} \lor z = \{A, B\})$
6		elvv	$⊢ z \in (V \times V) \leftrightarrow \exists x \exists y z = ⟨x, y⟩$
7	5 6	imbi12i	$⊢ (z \in ⟨A, B⟩ \to z \in (V \times V)) \leftrightarrow ((z = \{A\} \lor z = \{A, B\}) \to \exists x \exists y z = ⟨x, y⟩)$
8		jaob	$⊢ ((z = \{A\} \lor z = \{A, B\}) \to \exists x \exists y z = ⟨x, y⟩) \leftrightarrow ((z = \{A\} \to \exists x \exists y z = ⟨x, y⟩) \land (z = \{A, B\} \to \exists x \exists y z = ⟨x, y⟩))$
9	7 8	bitri	$⊢ (z \in ⟨A, B⟩ \to z \in (V \times V)) \leftrightarrow ((z = \{A\} \to \exists x \exists y z = ⟨x, y⟩) \land (z = \{A, B\} \to \exists x \exists y z = ⟨x, y⟩))$
10	9	albii	$⊢ \forall z (z \in ⟨A, B⟩ \to z \in (V \times V)) \leftrightarrow \forall z ((z = \{A\} \to \exists x \exists y z = ⟨x, y⟩) \land (z = \{A, B\} \to \exists x \exists y z = ⟨x, y⟩))$
11		19.26	$⊢ \forall z ((z = \{A\} \to \exists x \exists y z = ⟨x, y⟩) \land (z = \{A, B\} \to \exists x \exists y z = ⟨x, y⟩)) \leftrightarrow (\forall z (z = \{A\} \to \exists x \exists y z = ⟨x, y⟩) \land \forall z (z = \{A, B\} \to \exists x \exists y z = ⟨x, y⟩))$
12	10 11	bitri	$⊢ \forall z (z \in ⟨A, B⟩ \to z \in (V \times V)) \leftrightarrow (\forall z (z = \{A\} \to \exists x \exists y z = ⟨x, y⟩) \land \forall z (z = \{A, B\} \to \exists x \exists y z = ⟨x, y⟩))$
13	4 12	bitri	$⊢ ⟨A, B⟩ \subseteq V \times V \leftrightarrow (\forall z (z = \{A\} \to \exists x \exists y z = ⟨x, y⟩) \land \forall z (z = \{A, B\} \to \exists x \exists y z = ⟨x, y⟩))$
14		snex	$⊢ \{A\} \in V$
15		eqeq1	$⊢ z = \{A\} \to (z = \{A\} \leftrightarrow \{A\} = \{A\})$
16		eqeq1	$⊢ z = \{A\} \to (z = ⟨x, y⟩ \leftrightarrow \{A\} = ⟨x, y⟩)$
17		eqcom	$⊢ \{A\} = ⟨x, y⟩ \leftrightarrow ⟨x, y⟩ = \{A\}$
18		vex	$⊢ x \in V$
19		vex	$⊢ y \in V$
20	18 19	opeqsn	$⊢ ⟨x, y⟩ = \{A\} \leftrightarrow (x = y \land A = \{x\})$
21	17 20	bitri	$⊢ \{A\} = ⟨x, y⟩ \leftrightarrow (x = y \land A = \{x\})$
22	16 21	bitrdi	$⊢ z = \{A\} \to (z = ⟨x, y⟩ \leftrightarrow (x = y \land A = \{x\}))$
23	22	2exbidv	$⊢ z = \{A\} \to (\exists x \exists y z = ⟨x, y⟩ \leftrightarrow \exists x \exists y (x = y \land A = \{x\}))$
24	15 23	imbi12d	$⊢ z = \{A\} \to ((z = \{A\} \to \exists x \exists y z = ⟨x, y⟩) \leftrightarrow (\{A\} = \{A\} \to \exists x \exists y (x = y \land A = \{x\})))$
25	14 24	spcv	$⊢ \forall z (z = \{A\} \to \exists x \exists y z = ⟨x, y⟩) \to (\{A\} = \{A\} \to \exists x \exists y (x = y \land A = \{x\}))$
26		sneq	$⊢ w = x \to \{w\} = \{x\}$
27	26	eqeq2d	$⊢ w = x \to (A = \{w\} \leftrightarrow A = \{x\})$
28	27	cbvexvw	$⊢ \exists w A = \{w\} \leftrightarrow \exists x A = \{x\}$
29		ax6evr	$⊢ \exists y x = y$
30		19.41v	$⊢ \exists y (x = y \land A = \{x\}) \leftrightarrow (\exists y x = y \land A = \{x\})$
31	29 30	mpbiran	$⊢ \exists y (x = y \land A = \{x\}) \leftrightarrow A = \{x\}$
32	31	exbii	$⊢ \exists x \exists y (x = y \land A = \{x\}) \leftrightarrow \exists x A = \{x\}$
33		eqid	$⊢ \{A\} = \{A\}$
34	33	a1bi	$⊢ \exists x \exists y (x = y \land A = \{x\}) \leftrightarrow (\{A\} = \{A\} \to \exists x \exists y (x = y \land A = \{x\}))$
35	28 32 34	3bitr2ri	$⊢ (\{A\} = \{A\} \to \exists x \exists y (x = y \land A = \{x\})) \leftrightarrow \exists w A = \{w\}$
36	25 35	sylib	$⊢ \forall z (z = \{A\} \to \exists x \exists y z = ⟨x, y⟩) \to \exists w A = \{w\}$
37		eqid	$⊢ \{A, B\} = \{A, B\}$
38		prex	$⊢ \{A, B\} \in V$
39		eqeq1	$⊢ z = \{A, B\} \to (z = \{A, B\} \leftrightarrow \{A, B\} = \{A, B\})$
40		eqeq1	$⊢ z = \{A, B\} \to (z = ⟨x, y⟩ \leftrightarrow \{A, B\} = ⟨x, y⟩)$
41	40	2exbidv	$⊢ z = \{A, B\} \to (\exists x \exists y z = ⟨x, y⟩ \leftrightarrow \exists x \exists y \{A, B\} = ⟨x, y⟩)$
42	39 41	imbi12d	$⊢ z = \{A, B\} \to ((z = \{A, B\} \to \exists x \exists y z = ⟨x, y⟩) \leftrightarrow (\{A, B\} = \{A, B\} \to \exists x \exists y \{A, B\} = ⟨x, y⟩))$
43	38 42	spcv	$⊢ \forall z (z = \{A, B\} \to \exists x \exists y z = ⟨x, y⟩) \to (\{A, B\} = \{A, B\} \to \exists x \exists y \{A, B\} = ⟨x, y⟩)$
44	37 43	mpi	$⊢ \forall z (z = \{A, B\} \to \exists x \exists y z = ⟨x, y⟩) \to \exists x \exists y \{A, B\} = ⟨x, y⟩$
45		eqcom	$⊢ \{A, B\} = ⟨x, y⟩ \leftrightarrow ⟨x, y⟩ = \{A, B\}$
46	18 19 1 2	opeqpr	$⊢ ⟨x, y⟩ = \{A, B\} \leftrightarrow ((A = \{x\} \land B = \{x, y\}) \lor (A = \{x, y\} \land B = \{x\}))$
47	45 46	bitri	$⊢ \{A, B\} = ⟨x, y⟩ \leftrightarrow ((A = \{x\} \land B = \{x, y\}) \lor (A = \{x, y\} \land B = \{x\}))$
48		idd	$⊢ A = \{w\} \to ((A = \{x\} \land B = \{x, y\}) \to (A = \{x\} \land B = \{x, y\}))$
49		eqtr2	$⊢ (A = \{x, y\} \land A = \{w\}) \to \{x, y\} = \{w\}$
50	18 19	preqsn	$⊢ \{x, y\} = \{w\} \leftrightarrow (x = y \land y = w)$
51	50	simplbi	$⊢ \{x, y\} = \{w\} \to x = y$
52	49 51	syl	$⊢ (A = \{x, y\} \land A = \{w\}) \to x = y$
53		dfsn2	$⊢ \{x\} = \{x, x\}$
54		preq2	$⊢ x = y \to \{x, x\} = \{x, y\}$
55	53 54	eqtr2id	$⊢ x = y \to \{x, y\} = \{x\}$
56	55	eqeq2d	$⊢ x = y \to (A = \{x, y\} \leftrightarrow A = \{x\})$
57	53 54	eqtrid	$⊢ x = y \to \{x\} = \{x, y\}$
58	57	eqeq2d	$⊢ x = y \to (B = \{x\} \leftrightarrow B = \{x, y\})$
59	56 58	anbi12d	$⊢ x = y \to ((A = \{x, y\} \land B = \{x\}) \leftrightarrow (A = \{x\} \land B = \{x, y\}))$
60	59	biimpd	$⊢ x = y \to ((A = \{x, y\} \land B = \{x\}) \to (A = \{x\} \land B = \{x, y\}))$
61	60	expd	$⊢ x = y \to (A = \{x, y\} \to (B = \{x\} \to (A = \{x\} \land B = \{x, y\})))$
62	61	com12	$⊢ A = \{x, y\} \to (x = y \to (B = \{x\} \to (A = \{x\} \land B = \{x, y\})))$
63	62	adantr	$⊢ (A = \{x, y\} \land A = \{w\}) \to (x = y \to (B = \{x\} \to (A = \{x\} \land B = \{x, y\})))$
64	52 63	mpd	$⊢ (A = \{x, y\} \land A = \{w\}) \to (B = \{x\} \to (A = \{x\} \land B = \{x, y\}))$
65	64	expcom	$⊢ A = \{w\} \to (A = \{x, y\} \to (B = \{x\} \to (A = \{x\} \land B = \{x, y\})))$
66	65	impd	$⊢ A = \{w\} \to ((A = \{x, y\} \land B = \{x\}) \to (A = \{x\} \land B = \{x, y\}))$
67	48 66	jaod	$⊢ A = \{w\} \to (((A = \{x\} \land B = \{x, y\}) \lor (A = \{x, y\} \land B = \{x\})) \to (A = \{x\} \land B = \{x, y\}))$
68	47 67	biimtrid	$⊢ A = \{w\} \to (\{A, B\} = ⟨x, y⟩ \to (A = \{x\} \land B = \{x, y\}))$
69	68	2eximdv	$⊢ A = \{w\} \to (\exists x \exists y \{A, B\} = ⟨x, y⟩ \to \exists x \exists y (A = \{x\} \land B = \{x, y\}))$
70	69	exlimiv	$⊢ \exists w A = \{w\} \to (\exists x \exists y \{A, B\} = ⟨x, y⟩ \to \exists x \exists y (A = \{x\} \land B = \{x, y\}))$
71	70	imp	$⊢ (\exists w A = \{w\} \land \exists x \exists y \{A, B\} = ⟨x, y⟩) \to \exists x \exists y (A = \{x\} \land B = \{x, y\})$
72	36 44 71	syl2an	$⊢ (\forall z (z = \{A\} \to \exists x \exists y z = ⟨x, y⟩) \land \forall z (z = \{A, B\} \to \exists x \exists y z = ⟨x, y⟩)) \to \exists x \exists y (A = \{x\} \land B = \{x, y\})$
73	13 72	sylbi	$⊢ ⟨A, B⟩ \subseteq V \times V \to \exists x \exists y (A = \{x\} \land B = \{x, y\})$
74		simpr	$⊢ (A = \{x\} \land z = \{A\}) \to z = \{A\}$
75		equid	$⊢ x = x$
76	75	jctl	$⊢ A = \{x\} \to (x = x \land A = \{x\})$
77	18 18	opeqsn	$⊢ ⟨x, x⟩ = \{A\} \leftrightarrow (x = x \land A = \{x\})$
78	76 77	sylibr	$⊢ A = \{x\} \to ⟨x, x⟩ = \{A\}$
79	78	adantr	$⊢ (A = \{x\} \land z = \{A\}) \to ⟨x, x⟩ = \{A\}$
80	74 79	eqtr4d	$⊢ (A = \{x\} \land z = \{A\}) \to z = ⟨x, x⟩$
81		opeq12	$⊢ (w = x \land v = x) \to ⟨w, v⟩ = ⟨x, x⟩$
82	81	eqeq2d	$⊢ (w = x \land v = x) \to (z = ⟨w, v⟩ \leftrightarrow z = ⟨x, x⟩)$
83	18 18 82	spc2ev	$⊢ z = ⟨x, x⟩ \to \exists w \exists v z = ⟨w, v⟩$
84	80 83	syl	$⊢ (A = \{x\} \land z = \{A\}) \to \exists w \exists v z = ⟨w, v⟩$
85	84	adantlr	$⊢ ((A = \{x\} \land B = \{x, y\}) \land z = \{A\}) \to \exists w \exists v z = ⟨w, v⟩$
86		preq12	$⊢ (A = \{x\} \land B = \{x, y\}) \to \{A, B\} = \{\{x\}, \{x, y\}\}$
87	86	eqeq2d	$⊢ (A = \{x\} \land B = \{x, y\}) \to (z = \{A, B\} \leftrightarrow z = \{\{x\}, \{x, y\}\})$
88	87	biimpa	$⊢ ((A = \{x\} \land B = \{x, y\}) \land z = \{A, B\}) \to z = \{\{x\}, \{x, y\}\}$
89	18 19	dfop	$⊢ ⟨x, y⟩ = \{\{x\}, \{x, y\}\}$
90	88 89	eqtr4di	$⊢ ((A = \{x\} \land B = \{x, y\}) \land z = \{A, B\}) \to z = ⟨x, y⟩$
91		opeq12	$⊢ (w = x \land v = y) \to ⟨w, v⟩ = ⟨x, y⟩$
92	91	eqeq2d	$⊢ (w = x \land v = y) \to (z = ⟨w, v⟩ \leftrightarrow z = ⟨x, y⟩)$
93	18 19 92	spc2ev	$⊢ z = ⟨x, y⟩ \to \exists w \exists v z = ⟨w, v⟩$
94	90 93	syl	$⊢ ((A = \{x\} \land B = \{x, y\}) \land z = \{A, B\}) \to \exists w \exists v z = ⟨w, v⟩$
95	85 94	jaodan	$⊢ ((A = \{x\} \land B = \{x, y\}) \land (z = \{A\} \lor z = \{A, B\})) \to \exists w \exists v z = ⟨w, v⟩$
96	95	ex	$⊢ (A = \{x\} \land B = \{x, y\}) \to ((z = \{A\} \lor z = \{A, B\}) \to \exists w \exists v z = ⟨w, v⟩)$
97		elvv	$⊢ z \in (V \times V) \leftrightarrow \exists w \exists v z = ⟨w, v⟩$
98	96 5 97	3imtr4g	$⊢ (A = \{x\} \land B = \{x, y\}) \to (z \in ⟨A, B⟩ \to z \in (V \times V))$
99	98	ssrdv	$⊢ (A = \{x\} \land B = \{x, y\}) \to ⟨A, B⟩ \subseteq V \times V$
100	99	exlimivv	$⊢ \exists x \exists y (A = \{x\} \land B = \{x, y\}) \to ⟨A, B⟩ \subseteq V \times V$
101	73 100	impbii	$⊢ ⟨A, B⟩ \subseteq V \times V \leftrightarrow \exists x \exists y (A = \{x\} \land B = \{x, y\})$
102	3 101	bitri	$⊢ Rel ⟨A, B⟩ \leftrightarrow \exists x \exists y (A = \{x\} \land B = \{x, y\})$

Metamath Proof Explorer

Theorem relop

Proof