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 simpr ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) )
21 20 9 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ )
22 21 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ )
23 4 biimpar ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → 𝜓 )
24 22 23 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
25 trud ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → ⊤ )
26 24 25 2thd ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) ) → ( ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ⊤ ) )
27 26 3anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) ∧ 𝑐 = 𝐶 ) → ( ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ⊤ ) )
28 19 27 sbcied ⊢ ( ( ( 𝜑 ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ⊤ ) )
29 18 28 sbcied ⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → ( [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ⊤ ) )
30 1 29 sbcied ⊢ ( 𝜑 → ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ⊤ ) )
31 17 30 mpbiri ⊢ ( 𝜑 → [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
32 31 spesbcd ⊢ ( 𝜑 → ∃ 𝑎 [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
33 nfcv ⊢ Ⅎ 𝑏 𝐵
34 nfsbc1v ⊢ Ⅎ 𝑏 [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 )
35 34 nfex ⊢ Ⅎ 𝑏 ∃ 𝑎 [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 )
36 sbceq1a ⊢ ( 𝑏 = 𝐵 → ( [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
37 36 exbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑎 [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
38 33 35 37 spcegf ⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑎 [ 𝐵 / 𝑏 ] [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) → ∃ 𝑏 ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
39 2 32 38 sylc ⊢ ( 𝜑 → ∃ 𝑏 ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
40 nfcv ⊢ Ⅎ 𝑐 𝐶
41 nfsbc1v ⊢ Ⅎ 𝑐 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 )
42 41 nfex ⊢ Ⅎ 𝑐 ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 )
43 42 nfex ⊢ Ⅎ 𝑐 ∃ 𝑏 ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 )
44 sbceq1a ⊢ ( 𝑐 = 𝐶 → ( ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
45 44 2exbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑏 ∃ 𝑎 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑏 ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
46 40 43 45 spcegf ⊢ ( 𝐶 ∈ 𝑊 → ( ∃ 𝑏 ∃ 𝑎 [ 𝐶 / 𝑐 ] ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) → ∃ 𝑐 ∃ 𝑏 ∃ 𝑎 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
47 3 39 46 sylc ⊢ ( 𝜑 → ∃ 𝑐 ∃ 𝑏 ∃ 𝑎 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
48 excom13 ⊢ ( ∃ 𝑐 ∃ 𝑏 ∃ 𝑎 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
49 47 48 sylib ⊢ ( 𝜑 → ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )
50 eqeq1 ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
51 50 anbi1d ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
52 51 3exbidv ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
53 49 52 syl5ibrcom ⊢ ( 𝜑 → ( 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ) )
54 16 53 impbid ⊢ ( 𝜑 → ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) )
55 54 alrimiv ⊢ ( 𝜑 → ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) )
56 otex ⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∈ V
57 eqeq2 ⊢ ( 𝑦 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( 𝑥 = 𝑦 ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) )
58 57 bibi2d ⊢ ( 𝑦 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = 𝑦 ) ↔ ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) )
59 58 albidv ⊢ ( 𝑦 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) )
60 56 59 spcev ⊢ ( ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) → ∃ 𝑦 ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = 𝑦 ) )
61 55 60 syl ⊢ ( 𝜑 → ∃ 𝑦 ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = 𝑦 ) )
62 eu6 ⊢ ( ∃! 𝑥 ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑦 ∀ 𝑥 ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) ↔ 𝑥 = 𝑦 ) )
63 61 62 sylibr ⊢ ( 𝜑 → ∃! 𝑥 ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )