Theorem euotd 3961

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 3937	. . . 4 ⊢ ((A ∈ V ∧ B ∈ V ∧ 𝐶 ∈ V) → ⟨A, B, 𝐶⟩ ∈ V)
5	1, 2, 3, 4	syl3anc 1119	. . 3 ⊢ (φ → ⟨A, B, 𝐶⟩ ∈ V)
6		euotd.4	. . . . . . . . . . . . 13 ⊢ (φ → (ψ ↔ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)))
7	6	biimpa 280	. . . . . . . . . . . 12 ⊢ ((φ ∧ ψ) → (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶))
8		vex 2534	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
9		vex 2534	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ V
10		vex 2534	. . . . . . . . . . . . 13 ⊢ 𝑐 ∈ V
11	8, 9, 10	otth 3949	. . . . . . . . . . . 12 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ = ⟨A, B, 𝐶⟩ ↔ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶))
12	7, 11	sylibr 137	. . . . . . . . . . 11 ⊢ ((φ ∧ ψ) → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨A, B, 𝐶⟩)
13	12	eqeq2d 2029	. . . . . . . . . 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 1678	. . . . . 6 ⊢ (φ → (∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) → x = ⟨A, B, 𝐶⟩))
18	17	exlimdvv 1755	. . . . 5 ⊢ (φ → (∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) → x = ⟨A, B, 𝐶⟩))
19		tru 1230	. . . . . . . . . . 11 ⊢ ⊤
20	2	adantr 261	. . . . . . . . . . . . 13 ⊢ ((φ ∧ 𝑎 = A) → B ∈ V)
21	3	ad2antrr 460	. . . . . . . . . . . . . 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 2023	. . . . . . . . . . . . . . . . 17 ⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)) → ⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩)
25	6	biimpar 281	. . . . . . . . . . . . . . . . 17 ⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)) → ψ)
26	24, 25	jca 290	. . . . . . . . . . . . . . . 16 ⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)) → (⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
27		a1tru 1242	. . . . . . . . . . . . . . . 16 ⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)) → ⊤ )
28	26, 27	2thd 164	. . . . . . . . . . . . . . 15 ⊢ ((φ ∧ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶)) → ((⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ⊤ ))
29	28	3anassrs 1110	. . . . . . . . . . . . . 14 ⊢ ((((φ ∧ 𝑎 = A) ∧ 𝑏 = B) ∧ 𝑐 = 𝐶) → ((⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ⊤ ))
30	21, 29	sbcied 2772	. . . . . . . . . . . . 13 ⊢ (((φ ∧ 𝑎 = A) ∧ 𝑏 = B) → ([𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ⊤ ))
31	20, 30	sbcied 2772	. . . . . . . . . . . 12 ⊢ ((φ ∧ 𝑎 = A) → ([B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ⊤ ))
32	1, 31	sbcied 2772	. . . . . . . . . . 11 ⊢ (φ → ([A / 𝑎][B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ⊤ ))
33	19, 32	mpbiri 157	. . . . . . . . . 10 ⊢ (φ → [A / 𝑎][B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
34	33	spesbcd 2817	. . . . . . . . 9 ⊢ (φ → ∃𝑎[B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
35		nfcv 2156	. . . . . . . . . 10 ⊢ Ⅎ𝑏B
36		nfsbc1v 2755	. . . . . . . . . . 11 ⊢ Ⅎ𝑏[B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)
37	36	nfex 1506	. . . . . . . . . 10 ⊢ Ⅎ𝑏∃𝑎[B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)
38		sbceq1a 2746	. . . . . . . . . . 11 ⊢ (𝑏 = B → ([𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ [B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
39	38	exbidv 1684	. . . . . . . . . 10 ⊢ (𝑏 = B → (∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ∃𝑎[B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
40	35, 37, 39	spcegf 2609	. . . . . . . . 9 ⊢ (B ∈ V → (∃𝑎[B / 𝑏][𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) → ∃𝑏∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
41	2, 34, 40	sylc 56	. . . . . . . 8 ⊢ (φ → ∃𝑏∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
42		nfcv 2156	. . . . . . . . 9 ⊢ Ⅎ𝑐𝐶
43		nfsbc1v 2755	. . . . . . . . . . 11 ⊢ Ⅎ𝑐[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)
44	43	nfex 1506	. . . . . . . . . 10 ⊢ Ⅎ𝑐∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)
45	44	nfex 1506	. . . . . . . . 9 ⊢ Ⅎ𝑐∃𝑏∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)
46		sbceq1a 2746	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → ((⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ [𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
47	46	2exbidv 1726	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (∃𝑏∃𝑎(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ∃𝑏∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
48	42, 45, 47	spcegf 2609	. . . . . . . 8 ⊢ (𝐶 ∈ V → (∃𝑏∃𝑎[𝐶 / 𝑐](⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) → ∃𝑐∃𝑏∃𝑎(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
49	3, 41, 48	sylc 56	. . . . . . 7 ⊢ (φ → ∃𝑐∃𝑏∃𝑎(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
50		excom13 1557	. . . . . . 7 ⊢ (∃𝑐∃𝑏∃𝑎(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ ∃𝑎∃𝑏∃𝑐(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
51	49, 50	sylib 127	. . . . . 6 ⊢ (φ → ∃𝑎∃𝑏∃𝑐(⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ))
52		eqeq1 2024	. . . . . . . 8 ⊢ (x = ⟨A, B, 𝐶⟩ → (x = ⟨𝑎, 𝑏, 𝑐⟩ ↔ ⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩))
53	52	anbi1d 441	. . . . . . 7 ⊢ (x = ⟨A, B, 𝐶⟩ → ((x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ (⟨A, B, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)))
54	53	3exbidv 1727	. . . . . 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 1732	. . 3 ⊢ (φ → ∀x(∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = ⟨A, B, 𝐶⟩))
58		eqeq2 2027	. . . . . 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 1683	. . . 4 ⊢ (y = ⟨A, B, 𝐶⟩ → (∀x(∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = y) ↔ ∀x(∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ) ↔ x = ⟨A, B, 𝐶⟩)))
61	60	spcegv 2614	. . 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 1881	. 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 871  ∀wal 1224   = wceq 1226   ⊤ wtru 1227  ∃wex 1358   ∈ wcel 1370  ∃!weu 1878  Vcvv 2531  [wsbc 2737  ⟨cotp 3350

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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-rex 2286  df-v 2533  df-sbc 2738  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-ot 3356

This theorem is referenced by: (None)