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 ( 𝜑 → ∃! 𝑥𝑎𝑏𝑐 ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝜓 ) )