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		simpr	$⊢ (φ \land (a = A \land b = B \land c = C)) \to (a = A \land b = B \land c = C)$
21	20 9	sylibr	$⊢ (φ \land (a = A \land b = B \land c = C)) \to ⟨a, b, c⟩ = ⟨A, B, C⟩$
22	21	eqcomd	$⊢ (φ \land (a = A \land b = B \land c = C)) \to ⟨A, B, C⟩ = ⟨a, b, c⟩$
23	4	biimpar	$⊢ (φ \land (a = A \land b = B \land c = C)) \to ψ$
24	22 23	jca	$⊢ (φ \land (a = A \land b = B \land c = C)) \to (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
25		trud	$⊢ (φ \land (a = A \land b = B \land c = C)) \to ⊤$
26	24 25	2thd	$⊢ (φ \land (a = A \land b = B \land c = C)) \to ((⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow ⊤)$
27	26	3anassrs	$⊢ (((φ \land a = A) \land b = B) \land c = C) \to ((⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow ⊤)$
28	19 27	sbcied	$⊢ ((φ \land a = A) \land b = B) \to (\underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow ⊤)$
29	18 28	sbcied	$⊢ (φ \land a = A) \to (\underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow ⊤)$
30	1 29	sbcied	$⊢ φ \to (\underset{˙}{[} A / a \underset{˙}{]} \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow ⊤)$
31	17 30	mpbiri	$⊢ φ \to \underset{˙}{[} A / a \underset{˙}{]} \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
32	31	spesbcd	$⊢ φ \to \exists a \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
33		nfcv	$⊢ \underline{Ⅎ} b B$
34		nfsbc1v	$⊢ Ⅎ b \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
35	34	nfex	$⊢ Ⅎ b \exists a \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
36		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 ψ))$
37	36	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 ψ))$
38	33 35 37	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 ψ))$
39	2 32 38	sylc	$⊢ φ \to \exists b \exists a \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
40		nfcv	$⊢ \underline{Ⅎ} c C$
41		nfsbc1v	$⊢ Ⅎ c \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
42	41	nfex	$⊢ Ⅎ c \exists a \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
43	42	nfex	$⊢ Ⅎ c \exists b \exists a \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
44		sbceq1a	$⊢ c = C \to ((⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ) \leftrightarrow \underset{˙}{[} C / c \underset{˙}{]} (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ))$
45	44	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 ψ))$
46	40 43 45	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 ψ))$
47	3 39 46	sylc	$⊢ φ \to \exists c \exists b \exists a (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
48		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 ψ)$
49	47 48	sylib	$⊢ φ \to \exists a \exists b \exists c (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ)$
50		eqeq1	$⊢ x = ⟨A, B, C⟩ \to (x = ⟨a, b, c⟩ \leftrightarrow ⟨A, B, C⟩ = ⟨a, b, c⟩)$
51	50	anbi1d	$⊢ x = ⟨A, B, C⟩ \to ((x = ⟨a, b, c⟩ \land ψ) \leftrightarrow (⟨A, B, C⟩ = ⟨a, b, c⟩ \land ψ))$
52	51	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 ψ))$
53	49 52	syl5ibrcom	$⊢ φ \to (x = ⟨A, B, C⟩ \to \exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ))$
54	16 53	impbid	$⊢ φ \to (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = ⟨A, B, C⟩)$
55	54	alrimiv	$⊢ φ \to \forall x (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = ⟨A, B, C⟩)$
56		otex	$⊢ ⟨A, B, C⟩ \in V$
57		eqeq2	$⊢ y = ⟨A, B, C⟩ \to (x = y \leftrightarrow x = ⟨A, B, C⟩)$
58	57	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⟩))$
59	58	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⟩))$
60	56 59	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)$
61	55 60	syl	$⊢ φ \to \exists y \forall x (\exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ) \leftrightarrow x = y)$
62		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)$
63	61 62	sylibr	$⊢ φ \to \exists! x \exists a \exists b \exists c (x = ⟨a, b, c⟩ \land ψ)$

Metamath Proof Explorer

Theorem euotd

Proof