Metamath Proof Explorer

Theorem euotd

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

Ref Expression
Hypotheses euotd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
euotd.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
euotd.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
euotd.4 ⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) )
Assertion euotd ( 𝜑 → ∃! 𝑥 ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 euotd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
2 euotd.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3 euotd.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
4 euotd.4 ⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) )
5 4 biimpa ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) )
6 vex ⊢ 𝑎 ∈ V
7 vex ⊢ 𝑏 ∈ V
8 vex ⊢ 𝑐 ∈ V
9 6 7 8 otth ⊢ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ↔ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) )
10 5 9 sylibr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ )
11 10 eqeq2d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) )
12 11 biimpd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) )
13 12 impancom ⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → ( 𝜓 → 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) )
14 13 expimpd ⊢ ( 𝜑 → ( ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) → 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) )
15 14 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) → 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) )
16 15 exlimdvv ⊢ ( 𝜑 → ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) → 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) )
17 tru ⊢ ⊤
18 2 adantr ⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → 𝐵 ∈ 𝑉 )
19 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → 𝐶 ∈ 𝑊 )
20 9 bilanri ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ )
21 20 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ )
22 4 biimpar ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → 𝜓 )
23 21 22 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
24 trud ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → ⊤ )
25 23 24 2thd ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → ( ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ⊤ ) )
26 25 3anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) → ( ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ⊤ ) )
27 19 26 sbcied ⊢ ( ( ( 𝜑 ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ⊤ ) )
28 18 27 sbcied ⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → ( [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ⊤ ) )
29 1 28 sbcied ⊢ ( 𝜑 → ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ⊤ ) )
30 17 29 mpbiri ⊢ ( 𝜑 → [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
31 30 spesbcd ⊢ ( 𝜑 → ∃ 𝑎 [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
32 nfcv ⊢ Ⅎ 𝑏 𝐵
33 nfsbc1v ⊢ Ⅎ 𝑏 [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 )
34 33 nfex ⊢ Ⅎ 𝑏 ∃ 𝑎 [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 )
35 sbceq1a ⊢ ( 𝑏 = 𝐵 → ( [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
36 35 exbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑎 [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
37 32 34 36 spcegf ⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑎 [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) → ∃ 𝑏 ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
38 2 31 37 sylc ⊢ ( 𝜑 → ∃ 𝑏 ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
39 nfcv ⊢ Ⅎ 𝑐 𝐶
40 nfsbc1v ⊢ Ⅎ 𝑐 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 )
41 40 nfex ⊢ Ⅎ 𝑐 ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 )
42 41 nfex ⊢ Ⅎ 𝑐 ∃ 𝑏 ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 )
43 sbceq1a ⊢ ( 𝑐 = 𝐶 → ( ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
44 43 2exbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑏 ∃ 𝑎 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑏 ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
45 39 42 44 spcegf ⊢ ( 𝐶 ∈ 𝑊 → ( ∃ 𝑏 ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) → ∃ 𝑐 ∃ 𝑏 ∃ 𝑎 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
46 3 38 45 sylc ⊢ ( 𝜑 → ∃ 𝑐 ∃ 𝑏 ∃ 𝑎 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
47 excom13 ⊢ ( ∃ 𝑐 ∃ 𝑏 ∃ 𝑎 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
48 46 47 sylib ⊢ ( 𝜑 → ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
49 eqeq1 ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
50 49 anbi1d ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
51 50 3exbidv ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
52 48 51 syl5ibrcom ⊢ ( 𝜑 → ( 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
53 16 52 impbid ⊢ ( 𝜑 → ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) )
54 53 alrimiv ⊢ ( 𝜑 → ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) )
55 otex ⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∈ V
56 eqeq2 ⊢ ( 𝑦 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( 𝑥 = 𝑦 ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) )
57 56 bibi2d ⊢ ( 𝑦 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = 𝑦 ) ↔ ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) )
58 57 albidv ⊢ ( 𝑦 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) )
59 55 58 spcev ⊢ ( ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) → ∃ 𝑦 ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = 𝑦 ) )
60 54 59 syl ⊢ ( 𝜑 → ∃ 𝑦 ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = 𝑦 ) )
61 eu6 ⊢ ( ∃! 𝑥 ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑦 ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = 𝑦 ) )
62 60 61 sylibr ⊢ ( 𝜑 → ∃! 𝑥 ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )