opiota

Description: The property of a uniquely specified ordered pair. The proof uses properties of the iota description binder. (Contributed by Mario Carneiro, 21-May-2015)

	Ref	Expression
Hypotheses	opiota.1	$⊢ I = (ι z \| \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ))$
	opiota.2	$⊢ X = 1^{st} (I)$
	opiota.3	$⊢ Y = 2^{nd} (I)$
	opiota.4	$⊢ x = C \to (φ \leftrightarrow ψ)$
	opiota.5	$⊢ y = D \to (ψ \leftrightarrow χ)$
Assertion	opiota	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to ((C \in A \land D \in B \land χ) \leftrightarrow (C = X \land D = Y))$

Proof

Step	Hyp	Ref	Expression
1		opiota.1	$⊢ I = (ι z \| \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ))$
2		opiota.2	$⊢ X = 1^{st} (I)$
3		opiota.3	$⊢ Y = 2^{nd} (I)$
4		opiota.4	$⊢ x = C \to (φ \leftrightarrow ψ)$
5		opiota.5	$⊢ y = D \to (ψ \leftrightarrow χ)$
6	4 5	ceqsrex2v	$⊢ (C \in A \land D \in B) \to (\exists x \in A \exists y \in B ((x = C \land y = D) \land φ) \leftrightarrow χ)$
7	6	bicomd	$⊢ (C \in A \land D \in B) \to (χ \leftrightarrow \exists x \in A \exists y \in B ((x = C \land y = D) \land φ))$
8		opex	$⊢ ⟨C, D⟩ \in V$
9	8	a1i	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to ⟨C, D⟩ \in V$
10		id	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ)$
11		eqeq1	$⊢ z = ⟨C, D⟩ \to (z = ⟨x, y⟩ \leftrightarrow ⟨C, D⟩ = ⟨x, y⟩)$
12		eqcom	$⊢ ⟨C, D⟩ = ⟨x, y⟩ \leftrightarrow ⟨x, y⟩ = ⟨C, D⟩$
13		vex	$⊢ x \in V$
14		vex	$⊢ y \in V$
15	13 14	opth	$⊢ ⟨x, y⟩ = ⟨C, D⟩ \leftrightarrow (x = C \land y = D)$
16	12 15	bitri	$⊢ ⟨C, D⟩ = ⟨x, y⟩ \leftrightarrow (x = C \land y = D)$
17	11 16	bitrdi	$⊢ z = ⟨C, D⟩ \to (z = ⟨x, y⟩ \leftrightarrow (x = C \land y = D))$
18	17	anbi1d	$⊢ z = ⟨C, D⟩ \to ((z = ⟨x, y⟩ \land φ) \leftrightarrow ((x = C \land y = D) \land φ))$
19	18	2rexbidv	$⊢ z = ⟨C, D⟩ \to (\exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \in A \exists y \in B ((x = C \land y = D) \land φ))$
20	19	adantl	$⊢ (\exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \land z = ⟨C, D⟩) \to (\exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \in A \exists y \in B ((x = C \land y = D) \land φ))$
21		nfeu1	$⊢ Ⅎ z \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ)$
22		nfvd	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to Ⅎ z \exists x \in A \exists y \in B ((x = C \land y = D) \land φ)$
23		nfcvd	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to \underline{Ⅎ} z ⟨C, D⟩$
24	9 10 20 21 22 23	iota2df	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to (\exists x \in A \exists y \in B ((x = C \land y = D) \land φ) \leftrightarrow (ι z \| \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ)) = ⟨C, D⟩)$
25		eqcom	$⊢ ⟨C, D⟩ = I \leftrightarrow I = ⟨C, D⟩$
26	1	eqeq1i	$⊢ I = ⟨C, D⟩ \leftrightarrow (ι z \| \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ)) = ⟨C, D⟩$
27	25 26	bitri	$⊢ ⟨C, D⟩ = I \leftrightarrow (ι z \| \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ)) = ⟨C, D⟩$
28	24 27	bitr4di	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to (\exists x \in A \exists y \in B ((x = C \land y = D) \land φ) \leftrightarrow ⟨C, D⟩ = I)$
29	7 28	sylan9bbr	$⊢ (\exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \land (C \in A \land D \in B)) \to (χ \leftrightarrow ⟨C, D⟩ = I)$
30	29	pm5.32da	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to (((C \in A \land D \in B) \land χ) \leftrightarrow ((C \in A \land D \in B) \land ⟨C, D⟩ = I))$
31		opelxpi	$⊢ (x \in A \land y \in B) \to ⟨x, y⟩ \in (A \times B)$
32		simpl	$⊢ (z = ⟨x, y⟩ \land φ) \to z = ⟨x, y⟩$
33	32	eleq1d	$⊢ (z = ⟨x, y⟩ \land φ) \to (z \in (A \times B) \leftrightarrow ⟨x, y⟩ \in (A \times B))$
34	31 33	syl5ibrcom	$⊢ (x \in A \land y \in B) \to ((z = ⟨x, y⟩ \land φ) \to z \in (A \times B))$
35	34	rexlimivv	$⊢ \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to z \in (A \times B)$
36	35	abssi	$⊢ \{z \| \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ)\} \subseteq A \times B$
37		iotacl	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to (ι z \| \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ)) \in \{z \| \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ)\}$
38	36 37	sselid	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to (ι z \| \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ)) \in (A \times B)$
39	1 38	eqeltrid	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to I \in (A \times B)$
40		opelxp	$⊢ ⟨C, D⟩ \in (A \times B) \leftrightarrow (C \in A \land D \in B)$
41		eleq1	$⊢ ⟨C, D⟩ = I \to (⟨C, D⟩ \in (A \times B) \leftrightarrow I \in (A \times B))$
42	40 41	bitr3id	$⊢ ⟨C, D⟩ = I \to ((C \in A \land D \in B) \leftrightarrow I \in (A \times B))$
43	39 42	syl5ibrcom	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to (⟨C, D⟩ = I \to (C \in A \land D \in B))$
44	43	pm4.71rd	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to (⟨C, D⟩ = I \leftrightarrow ((C \in A \land D \in B) \land ⟨C, D⟩ = I))$
45		1st2nd2	$⊢ I \in (A \times B) \to I = ⟨1^{st} (I), 2^{nd} (I)⟩$
46	39 45	syl	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to I = ⟨1^{st} (I), 2^{nd} (I)⟩$
47	46	eqeq2d	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to (⟨C, D⟩ = I \leftrightarrow ⟨C, D⟩ = ⟨1^{st} (I), 2^{nd} (I)⟩)$
48	30 44 47	3bitr2d	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to (((C \in A \land D \in B) \land χ) \leftrightarrow ⟨C, D⟩ = ⟨1^{st} (I), 2^{nd} (I)⟩)$
49		df-3an	$⊢ (C \in A \land D \in B \land χ) \leftrightarrow ((C \in A \land D \in B) \land χ)$
50	2	eqeq2i	$⊢ C = X \leftrightarrow C = 1^{st} (I)$
51	3	eqeq2i	$⊢ D = Y \leftrightarrow D = 2^{nd} (I)$
52	50 51	anbi12i	$⊢ (C = X \land D = Y) \leftrightarrow (C = 1^{st} (I) \land D = 2^{nd} (I))$
53		fvex	$⊢ 1^{st} (I) \in V$
54		fvex	$⊢ 2^{nd} (I) \in V$
55	53 54	opth2	$⊢ ⟨C, D⟩ = ⟨1^{st} (I), 2^{nd} (I)⟩ \leftrightarrow (C = 1^{st} (I) \land D = 2^{nd} (I))$
56	52 55	bitr4i	$⊢ (C = X \land D = Y) \leftrightarrow ⟨C, D⟩ = ⟨1^{st} (I), 2^{nd} (I)⟩$
57	48 49 56	3bitr4g	$⊢ \exists! z \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land φ) \to ((C \in A \land D \in B \land χ) \leftrightarrow (C = X \land D = Y))$

Metamath Proof Explorer

Theorem opiota

Proof