euotd

Description: Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015)

	Ref	Expression
Hypotheses	euotd.1	$⊢ φ \to A \in U$
	euotd.2	$⊢ φ \to B \in V$
	euotd.3	$⊢ φ \to C \in W$
	euotd.4	$⊢ φ \to (ψ \leftrightarrow (a = A \land b = B \land c = C))$
Assertion	euotd	$⊢ φ \to \exists! x \exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ)$

Proof

Step	Hyp	Ref	Expression
1		euotd.1	$⊢ φ \to A \in U$
2		euotd.2	$⊢ φ \to B \in V$
3		euotd.3	$⊢ φ \to C \in W$
4		euotd.4	$⊢ φ \to (ψ \leftrightarrow (a = A \land b = B \land c = C))$
5	4	biimpa	$⊢ (φ \land ψ) \to (a = A \land b = B \land c = C)$
6		vex	$⊢ a \in V$
7		vex	$⊢ b \in V$
8		vex	$⊢ c \in V$
9	6 7 8	otth	$⊢ ⟨a, b, c⟩ = ⟨A, B, C⟩ \leftrightarrow (a = A \land b = B \land c = C)$
10	5 9	sylibr	$⊢ (φ \land ψ) \to ⟨a, b, c⟩ = ⟨A, B, C⟩$
11	10	eqeq2d	$⊢ (φ \land ψ) \to (x = ⟨a, b, c⟩ \leftrightarrow x = ⟨A, B, C⟩)$
12	11	biimpd	$⊢ (φ \land ψ) \to (x = ⟨a, b, c⟩ \to x = ⟨A, B, C⟩)$
13	12	impancom	$⊢ (φ \land x = ⟨a, b, c⟩) \to (ψ \to x = ⟨A, B, C⟩)$
14	13	expimpd	$⊢ φ \to ((x = ⟨a, b, c⟩ \land ψ) \to x = ⟨A, B, C⟩)$
15	14	exlimdv	$⊢ φ \to (\exists c (x = ⟨a, b, c⟩ \land ψ) \to x = ⟨A, B, C⟩)$
16	15	exlimdvv	$⊢ φ \to (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \to x = ⟨A, B, C⟩)$
17		tru	$⊢ ⊤$
18	2	adantr	$⊢ (φ \land a = A) \to B \in V$
19	3	ad2antrr	$⊢ ((φ \land a = A) \land b = B) \to C \in W$
20	9	bilanri	$⊢ (φ \land (a = A \land b = B \land c = C)) \to ⟨a, b, c⟩ = ⟨A, B, C⟩$
21	20	eqcomd	$⊢ (φ \land (a = A \land b = B \land c = C)) \to ⟨A, B, C⟩ = ⟨a, b, c⟩$
22	4	biimpar	$⊢ (φ \land (a = A \land b = B \land c = C)) \to ψ$
23	21 22	jca	$⊢ (φ \land (a = A \land b = B \land c = C)) \to (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
24		trud	$⊢ (φ \land (a = A \land b = B \land c = C)) \to ⊤$
25	23 24	2thd	$⊢ (φ \land (a = A \land b = B \land c = C)) \to ((⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow ⊤)$
26	25	3anassrs	$⊢ (((φ \land a = A) \land b = B) \land c = C) \to ((⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow ⊤)$
27	19 26	sbcied	$⊢ ((φ \land a = A) \land b = B) \to (\underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow ⊤)$
28	18 27	sbcied	$⊢ (φ \land a = A) \to (\underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow ⊤)$
29	1 28	sbcied	$⊢ φ \to (\underset{˙}{[} A / a \underset{˙}{]} \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow ⊤)$
30	17 29	mpbiri	$⊢ φ \to \underset{˙}{[} A / a \underset{˙}{]} \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
31	30	spesbcd	$⊢ φ \to \exists a \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
32		nfcv	$⊢ \underline{Ⅎ} b B$
33		nfsbc1v	$⊢ Ⅎ b \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
34	33	nfex	$⊢ Ⅎ b \exists a \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
35		sbceq1a	$⊢ b = B \to (\underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ))$
36	35	exbidv	$⊢ b = B \to (\exists a \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow \exists a \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ))$
37	32 34 36	spcegf	$⊢ B \in V \to (\exists a \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \to \exists b \exists a \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ))$
38	2 31 37	sylc	$⊢ φ \to \exists b \exists a \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
39		nfcv	$⊢ \underline{Ⅎ} c C$
40		nfsbc1v	$⊢ Ⅎ c \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
41	40	nfex	$⊢ Ⅎ c \exists a \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
42	41	nfex	$⊢ Ⅎ c \exists b \exists a \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
43		sbceq1a	$⊢ c = C \to ((⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ))$
44	43	2exbidv	$⊢ c = C \to (\exists b \exists a (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow \exists b \exists a \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ))$
45	39 42 44	spcegf	$⊢ C \in W \to (\exists b \exists a \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \to \exists c \exists b \exists a (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ))$
46	3 38 45	sylc	$⊢ φ \to \exists c \exists b \exists a (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
47		excom13	$⊢ \exists c \exists b \exists a (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow \exists a \exists b \exists c (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
48	46 47	sylib	$⊢ φ \to \exists a \exists b \exists c (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
49		eqeq1	$⊢ x = ⟨A, B, C⟩ \to (x = ⟨a, b, c⟩ \leftrightarrow ⟨A, B, C⟩ = ⟨a, b, c⟩)$
50	49	anbi1d	$⊢ x = ⟨A, B, C⟩ \to ((x = ⟨a, b, c⟩ \land ψ) \leftrightarrow (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ))$
51	50	3exbidv	$⊢ x = ⟨A, B, C⟩ \to (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow \exists a \exists b \exists c (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ))$
52	48 51	syl5ibrcom	$⊢ φ \to (x = ⟨A, B, C⟩ \to \exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ))$
53	16 52	impbid	$⊢ φ \to (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = ⟨A, B, C⟩)$
54	53	alrimiv	$⊢ φ \to \forall x (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = ⟨A, B, C⟩)$
55		otex	$⊢ ⟨A, B, C⟩ \in V$
56		eqeq2	$⊢ y = ⟨A, B, C⟩ \to (x = y \leftrightarrow x = ⟨A, B, C⟩)$
57	56	bibi2d	$⊢ y = ⟨A, B, C⟩ \to ((\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = y) \leftrightarrow (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = ⟨A, B, C⟩))$
58	57	albidv	$⊢ y = ⟨A, B, C⟩ \to (\forall x (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = y) \leftrightarrow \forall x (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = ⟨A, B, C⟩))$
59	55 58	spcev	$⊢ \forall x (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = ⟨A, B, C⟩) \to \exists y \forall x (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = y)$
60	54 59	syl	$⊢ φ \to \exists y \forall x (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = y)$
61		eu6	$⊢ \exists! x \exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow \exists y \forall x (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = y)$
62	60 61	sylibr	$⊢ φ \to \exists! x \exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ)$

Metamath Proof Explorer

Theorem euotd

Proof