Theorem euotd 5430

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

Hypotheses

Ref	Expression
euotd.1	⊢ (𝜑 → 𝐴 ∈ 𝑈)
euotd.2	⊢ (𝜑 → 𝐵 ∈ 𝑉)
euotd.3	⊢ (𝜑 → 𝐶 ∈ 𝑊)
euotd.4	⊢ (𝜑 → (𝜓 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)))

Assertion

Ref	Expression
euotd	⊢ (𝜑 → ∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))

Distinct variable groups:   𝑎,𝑏,𝑐,𝑥,𝐴   𝐵,𝑎,𝑏,𝑐,𝑥   𝐶,𝑎,𝑏,𝑐,𝑥   𝜑,𝑎,𝑏,𝑐,𝑥

Allowed substitution hints:   𝜓(𝑥,𝑎,𝑏,𝑐)   𝑈(𝑥,𝑎,𝑏,𝑐)   𝑉(𝑥,𝑎,𝑏,𝑐)   𝑊(𝑥,𝑎,𝑏,𝑐)

Proof of Theorem euotd

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		euotd.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝜓 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)))
2	1	biimpa 477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶))
3		vex 3435	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
4		vex 3435	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ V
5		vex 3435	. . . . . . . . . . . . 13 ⊢ 𝑐 ∈ V
6	3, 4, 5	otth 5402	. . . . . . . . . . . 12 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝐴, 𝐵, 𝐶⟩ ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶))
7	2, 6	sylibr 233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝐴, 𝐵, 𝐶⟩)
8	7	eqeq2d 2751	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
9	8	biimpd 228	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
10	9	impancom 452	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 = ⟨𝑎, 𝑏, 𝑐⟩) → (𝜓 → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
11	10	expimpd 454	. . . . . . 7 ⊢ (𝜑 → ((𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
12	11	exlimdv 1940	. . . . . 6 ⊢ (𝜑 → (∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
13	12	exlimdvv 1941	. . . . 5 ⊢ (𝜑 → (∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
14		euotd.3	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ 𝑊)
15		euotd.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
16		tru 1546	. . . . . . . . . . 11 ⊢ ⊤
17		euotd.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
18	15	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 = 𝐴) → 𝐵 ∈ 𝑉)
19	14	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 = 𝐴) ∧ 𝑏 = 𝐵) → 𝐶 ∈ 𝑊)
20		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶))
21	20, 6	sylibr 233	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝐴, 𝐵, 𝐶⟩)
22	21	eqcomd 2746	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → ⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩)
23	1	biimpar 478	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → 𝜓)
24	22, 23	jca 512	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → (⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
25		trud 1552	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → ⊤)
26	24, 25	2thd 264	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → ((⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
27	26	3anassrs 1359	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 = 𝐴) ∧ 𝑏 = 𝐵) ∧ 𝑐 = 𝐶) → ((⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
28	19, 27	sbcied 3765	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 = 𝐴) ∧ 𝑏 = 𝐵) → ([𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
29	18, 28	sbcied 3765	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 = 𝐴) → ([𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
30	17, 29	sbcied 3765	. . . . . . . . . . 11 ⊢ (𝜑 → ([𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
31	16, 30	mpbiri 257	. . . . . . . . . 10 ⊢ (𝜑 → [𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
32	31	spesbcd 3821	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
33		nfcv 2909	. . . . . . . . . 10 ⊢ Ⅎ𝑏𝐵
34		nfsbc1v 3740	. . . . . . . . . . 11 ⊢ Ⅎ𝑏[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
35	34	nfex 2322	. . . . . . . . . 10 ⊢ Ⅎ𝑏∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
36		sbceq1a 3731	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → ([𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ [𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
37	36	exbidv 1928	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → (∃𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
38	33, 35, 37	spcegf 3530	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → (∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → ∃𝑏∃𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
39	15, 32, 38	sylc 65	. . . . . . . 8 ⊢ (𝜑 → ∃𝑏∃𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
40		nfcv 2909	. . . . . . . . 9 ⊢ Ⅎ𝑐𝐶
41		nfsbc1v 3740	. . . . . . . . . . 11 ⊢ Ⅎ𝑐[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
42	41	nfex 2322	. . . . . . . . . 10 ⊢ Ⅎ𝑐∃𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
43	42	nfex 2322	. . . . . . . . 9 ⊢ Ⅎ𝑐∃𝑏∃𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
44		sbceq1a 3731	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → ((⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ [𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
45	44	2exbidv 1931	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (∃𝑏∃𝑎(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑏∃𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
46	40, 43, 45	spcegf 3530	. . . . . . . 8 ⊢ (𝐶 ∈ 𝑊 → (∃𝑏∃𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → ∃𝑐∃𝑏∃𝑎(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
47	14, 39, 46	sylc 65	. . . . . . 7 ⊢ (𝜑 → ∃𝑐∃𝑏∃𝑎(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
48		excom13 2168	. . . . . . 7 ⊢ (∃𝑐∃𝑏∃𝑎(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑎∃𝑏∃𝑐(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
49	47, 48	sylib 217	. . . . . 6 ⊢ (𝜑 → ∃𝑎∃𝑏∃𝑐(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
50		eqeq1 2744	. . . . . . . 8 ⊢ (𝑥 = ⟨𝐴, 𝐵, 𝐶⟩ → (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ↔ ⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩))
51	50	anbi1d 630	. . . . . . 7 ⊢ (𝑥 = ⟨𝐴, 𝐵, 𝐶⟩ → ((𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ (⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
52	51	3exbidv 1932	. . . . . 6 ⊢ (𝑥 = ⟨𝐴, 𝐵, 𝐶⟩ → (∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑎∃𝑏∃𝑐(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
53	49, 52	syl5ibrcom 246	. . . . 5 ⊢ (𝜑 → (𝑥 = ⟨𝐴, 𝐵, 𝐶⟩ → ∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
54	13, 53	impbid 211	. . . 4 ⊢ (𝜑 → (∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
55	54	alrimiv 1934	. . 3 ⊢ (𝜑 → ∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
56		otex 5383	. . . 4 ⊢ ⟨𝐴, 𝐵, 𝐶⟩ ∈ V
57		eqeq2 2752	. . . . . 6 ⊢ (𝑦 = ⟨𝐴, 𝐵, 𝐶⟩ → (𝑥 = 𝑦 ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
58	57	bibi2d 343	. . . . 5 ⊢ (𝑦 = ⟨𝐴, 𝐵, 𝐶⟩ → ((∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦) ↔ (∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩)))
59	58	albidv 1927	. . . 4 ⊢ (𝑦 = ⟨𝐴, 𝐵, 𝐶⟩ → (∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦) ↔ ∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩)))
60	56, 59	spcev 3544	. . 3 ⊢ (∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩) → ∃𝑦∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦))
61	55, 60	syl 17	. 2 ⊢ (𝜑 → ∃𝑦∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦))
62		eu6 2576	. 2 ⊢ (∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑦∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦))
63	61, 62	sylibr 233	1 ⊢ (𝜑 → ∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086  ∀wal 1540   = wceq 1542  ⊤wtru 1543  ∃wex 1786   ∈ wcel 2110  ∃!weu 2570  [wsbc 3720  ⟨cotp 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-dif 3895  df-un 3897  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-ot 4576

This theorem is referenced by:  oeeu  8417