Theorem euotd 3982

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

Hypotheses

Ref	Expression
euotd.1	⊢ (φ → A ∈ V)
euotd.2	⊢ (φ → B ∈ V)
euotd.3	⊢ (φ → 𝐶 ∈ V)
euotd.4	⊢ (φ → (ψ ↔ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)))

Assertion

Ref	Expression
euotd	⊢ (φ → ∃!x∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))

Distinct variable groups:   𝑎,𝑏,𝑐,x,A   B,𝑎,𝑏,𝑐,x   𝐶,𝑎,𝑏,𝑐,x   φ,𝑎,𝑏,𝑐,x

Allowed substitution hints:   ψ(x,𝑎,𝑏,𝑐)

Proof of Theorem euotd

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		euotd.1	. . . 4 ⊢ (φ → A ∈ V)
2		euotd.2	. . . 4 ⊢ (φ → B ∈ V)
3		euotd.3	. . . 4 ⊢ (φ → 𝐶 ∈ V)
4		otexg 3958	. . . 4 ⊢ ((A ∈ V ∧ B ∈ V ∧ 𝐶 ∈ V) → ⟨A, B, 𝐶⟩ ∈ V)
5	1, 2, 3, 4	syl3anc 1134	. . 3 ⊢ (φ → ⟨A, B, 𝐶⟩ ∈ V)
6		euotd.4	. . . . . . . . . . . . 13 ⊢ (φ → (ψ ↔ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)))
7	6	biimpa 280	. . . . . . . . . . . 12 ⊢ ((φ ∧ ψ) → (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶))
8		vex 2554	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
9		vex 2554	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ V
10		vex 2554	. . . . . . . . . . . . 13 ⊢ 𝑐 ∈ V
11	8, 9, 10	otth 3970	. . . . . . . . . . . 12 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ = ⟨A, B, 𝐶⟩ ↔ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶))
12	7, 11	sylibr 137	. . . . . . . . . . 11 ⊢ ((φ ∧ ψ) → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨A, B, 𝐶⟩)
13	12	eqeq2d 2048	. . . . . . . . . 10 ⊢ ((φ ∧ ψ) → (x = ⟨𝑎, 𝑏, 𝑐⟩ ↔ x = ⟨A, B, 𝐶⟩))
14	13	biimpd 132	. . . . . . . . 9 ⊢ ((φ ∧ ψ) → (x = ⟨𝑎, 𝑏, 𝑐⟩ → x = ⟨A, B, 𝐶⟩))
15	14	impancom 247	. . . . . . . 8 ⊢ ((φ ∧ x = ⟨𝑎, 𝑏, 𝑐⟩) → (ψ → x = ⟨A, B, 𝐶⟩))
16	15	expimpd 345	. . . . . . 7 ⊢ (φ → ((x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) → x = ⟨A, B, 𝐶⟩))
17	16	exlimdv 1697	. . . . . 6 ⊢ (φ → (∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) → x = ⟨A, B, 𝐶⟩))
18	17	exlimdvv 1774	. . . . 5 ⊢ (φ → (∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) → x = ⟨A, B, 𝐶⟩))
19		tru 1246	. . . . . . . . . . 11 ⊢ ⊤
20	2	adantr 261	. . . . . . . . . . . . 13 ⊢ ((φ ∧ 𝑎 = A) → B ∈ V)
21	3	ad2antrr 457	. . . . . . . . . . . . . 14 ⊢ (((φ ∧ 𝑎 = A) ∧ 𝑏 = B) → 𝐶 ∈ V)
22		simpr 103	. . . . . . . . . . . . . . . . . . 19 ⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)) → (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶))
23	22, 11	sylibr 137	. . . . . . . . . . . . . . . . . 18 ⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)) → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨A, B, 𝐶⟩)
24	23	eqcomd 2042	. . . . . . . . . . . . . . . . 17 ⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)) → ⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩)
25	6	biimpar 281	. . . . . . . . . . . . . . . . 17 ⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)) → ψ)
26	24, 25	jca 290	. . . . . . . . . . . . . . . 16 ⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)) → (⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
27		a1tru 1258	. . . . . . . . . . . . . . . 16 ⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)) → ⊤ )
28	26, 27	2thd 164	. . . . . . . . . . . . . . 15 ⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)) → ((⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ⊤ ))
29	28	3anassrs 1125	. . . . . . . . . . . . . 14 ⊢ ((((φ ∧ 𝑎 = A) ∧ 𝑏 = B) ∧ 𝑐 = 𝐶) → ((⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ⊤ ))
30	21, 29	sbcied 2793	. . . . . . . . . . . . 13 ⊢ (((φ ∧ 𝑎 = A) ∧ 𝑏 = B) → ([𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ⊤ ))
31	20, 30	sbcied 2793	. . . . . . . . . . . 12 ⊢ ((φ ∧ 𝑎 = A) → ([B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ⊤ ))
32	1, 31	sbcied 2793	. . . . . . . . . . 11 ⊢ (φ → ([A / 𝑎][B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ⊤ ))
33	19, 32	mpbiri 157	. . . . . . . . . 10 ⊢ (φ → [A / 𝑎][B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
34	33	spesbcd 2838	. . . . . . . . 9 ⊢ (φ → ∃𝑎[B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
35		nfcv 2175	. . . . . . . . . 10 ⊢ Ⅎ𝑏B
36		nfsbc1v 2776	. . . . . . . . . . 11 ⊢ Ⅎ𝑏[B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)
37	36	nfex 1525	. . . . . . . . . 10 ⊢ Ⅎ𝑏∃𝑎[B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)
38		sbceq1a 2767	. . . . . . . . . . 11 ⊢ (𝑏 = B → ([𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ [B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
39	38	exbidv 1703	. . . . . . . . . 10 ⊢ (𝑏 = B → (∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ∃𝑎[B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
40	35, 37, 39	spcegf 2630	. . . . . . . . 9 ⊢ (B ∈ V → (∃𝑎[B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) → ∃𝑏∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
41	2, 34, 40	sylc 56	. . . . . . . 8 ⊢ (φ → ∃𝑏∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
42		nfcv 2175	. . . . . . . . 9 ⊢ Ⅎ𝑐𝐶
43		nfsbc1v 2776	. . . . . . . . . . 11 ⊢ Ⅎ𝑐[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)
44	43	nfex 1525	. . . . . . . . . 10 ⊢ Ⅎ𝑐∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)
45	44	nfex 1525	. . . . . . . . 9 ⊢ Ⅎ𝑐∃𝑏∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)
46		sbceq1a 2767	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → ((⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ [𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
47	46	2exbidv 1745	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (∃𝑏∃𝑎(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ∃𝑏∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
48	42, 45, 47	spcegf 2630	. . . . . . . 8 ⊢ (𝐶 ∈ V → (∃𝑏∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) → ∃𝑐∃𝑏∃𝑎(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
49	3, 41, 48	sylc 56	. . . . . . 7 ⊢ (φ → ∃𝑐∃𝑏∃𝑎(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
50		excom13 1576	. . . . . . 7 ⊢ (∃𝑐∃𝑏∃𝑎(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ∃𝑎∃𝑏∃𝑐(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
51	49, 50	sylib 127	. . . . . 6 ⊢ (φ → ∃𝑎∃𝑏∃𝑐(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
52		eqeq1 2043	. . . . . . . 8 ⊢ (x = ⟨A, B, 𝐶⟩ → (x = ⟨𝑎, 𝑏, 𝑐⟩ ↔ ⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩))
53	52	anbi1d 438	. . . . . . 7 ⊢ (x = ⟨A, B, 𝐶⟩ → ((x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ (⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
54	53	3exbidv 1746	. . . . . 6 ⊢ (x = ⟨A, B, 𝐶⟩ → (∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ∃𝑎∃𝑏∃𝑐(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
55	51, 54	syl5ibrcom 146	. . . . 5 ⊢ (φ → (x = ⟨A, B, 𝐶⟩ → ∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
56	18, 55	impbid 120	. . . 4 ⊢ (φ → (∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = ⟨A, B, 𝐶⟩))
57	56	alrimiv 1751	. . 3 ⊢ (φ → ∀x(∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = ⟨A, B, 𝐶⟩))
58		eqeq2 2046	. . . . . 6 ⊢ (y = ⟨A, B, 𝐶⟩ → (x = y ↔ x = ⟨A, B, 𝐶⟩))
59	58	bibi2d 221	. . . . 5 ⊢ (y = ⟨A, B, 𝐶⟩ → ((∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = y) ↔ (∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = ⟨A, B, 𝐶⟩)))
60	59	albidv 1702	. . . 4 ⊢ (y = ⟨A, B, 𝐶⟩ → (∀x(∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = y) ↔ ∀x(∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = ⟨A, B, 𝐶⟩)))
61	60	spcegv 2635	. . 3 ⊢ (⟨A, B, 𝐶⟩ ∈ V → (∀x(∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = ⟨A, B, 𝐶⟩) → ∃y∀x(∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = y)))
62	5, 57, 61	sylc 56	. 2 ⊢ (φ → ∃y∀x(∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = y))
63		df-eu 1900	. 2 ⊢ (∃!x∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ∃y∀x(∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = y))
64	62, 63	sylibr 137	1 ⊢ (φ → ∃!x∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884  ∀wal 1240   = wceq 1242   ⊤ wtru 1243  ∃wex 1378   ∈ wcel 1390  ∃!weu 1897  Vcvv 2551  [wsbc 2758  ⟨cotp 3371

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-ot 3377

This theorem is referenced by: (None)