MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  euotd Structured version   Visualization version   GIF version

Theorem euotd 5394
Description: Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.)
Hypotheses
Ref Expression
euotd.1 (𝜑𝐴 ∈ V)
euotd.2 (𝜑𝐵 ∈ V)
euotd.3 (𝜑𝐶 ∈ V)
euotd.4 (𝜑 → (𝜓 ↔ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)))
Assertion
Ref Expression
euotd (𝜑 → ∃!𝑥𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
Distinct variable groups:   𝑎,𝑏,𝑐,𝑥,𝐴   𝐵,𝑎,𝑏,𝑐,𝑥   𝐶,𝑎,𝑏,𝑐,𝑥   𝜑,𝑎,𝑏,𝑐,𝑥
Allowed substitution hints:   𝜓(𝑥,𝑎,𝑏,𝑐)

Proof of Theorem euotd
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 euotd.4 . . . . . . . . . . . . 13 (𝜑 → (𝜓 ↔ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)))
21biimpa 477 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶))
3 vex 3495 . . . . . . . . . . . . 13 𝑎 ∈ V
4 vex 3495 . . . . . . . . . . . . 13 𝑏 ∈ V
5 vex 3495 . . . . . . . . . . . . 13 𝑐 ∈ V
63, 4, 5otth 5367 . . . . . . . . . . . 12 (⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝐴, 𝐵, 𝐶⟩ ↔ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶))
72, 6sylibr 235 . . . . . . . . . . 11 ((𝜑𝜓) → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝐴, 𝐵, 𝐶⟩)
87eqeq2d 2829 . . . . . . . . . 10 ((𝜑𝜓) → (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
98biimpd 230 . . . . . . . . 9 ((𝜑𝜓) → (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
109impancom 452 . . . . . . . 8 ((𝜑𝑥 = ⟨𝑎, 𝑏, 𝑐⟩) → (𝜓𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
1110expimpd 454 . . . . . . 7 (𝜑 → ((𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
1211exlimdv 1925 . . . . . 6 (𝜑 → (∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
1312exlimdvv 1926 . . . . 5 (𝜑 → (∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
14 euotd.3 . . . . . . . 8 (𝜑𝐶 ∈ V)
15 euotd.2 . . . . . . . . 9 (𝜑𝐵 ∈ V)
16 tru 1532 . . . . . . . . . . 11
17 euotd.1 . . . . . . . . . . . 12 (𝜑𝐴 ∈ V)
1815adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑎 = 𝐴) → 𝐵 ∈ V)
1914ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑𝑎 = 𝐴) ∧ 𝑏 = 𝐵) → 𝐶 ∈ V)
20 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶))
2120, 6sylibr 235 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝐴, 𝐵, 𝐶⟩)
2221eqcomd 2824 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → ⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩)
231biimpar 478 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → 𝜓)
2422, 23jca 512 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → (⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
25 trud 1538 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → ⊤)
2624, 252thd 266 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → ((⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
27263anassrs 1352 . . . . . . . . . . . . . 14 ((((𝜑𝑎 = 𝐴) ∧ 𝑏 = 𝐵) ∧ 𝑐 = 𝐶) → ((⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
2819, 27sbcied 3811 . . . . . . . . . . . . 13 (((𝜑𝑎 = 𝐴) ∧ 𝑏 = 𝐵) → ([𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
2918, 28sbcied 3811 . . . . . . . . . . . 12 ((𝜑𝑎 = 𝐴) → ([𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
3017, 29sbcied 3811 . . . . . . . . . . 11 (𝜑 → ([𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
3116, 30mpbiri 259 . . . . . . . . . 10 (𝜑[𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
3231spesbcd 3863 . . . . . . . . 9 (𝜑 → ∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
33 nfcv 2974 . . . . . . . . . 10 𝑏𝐵
34 nfsbc1v 3789 . . . . . . . . . . 11 𝑏[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
3534nfex 2334 . . . . . . . . . 10 𝑏𝑎[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
36 sbceq1a 3780 . . . . . . . . . . 11 (𝑏 = 𝐵 → ([𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ [𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
3736exbidv 1913 . . . . . . . . . 10 (𝑏 = 𝐵 → (∃𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
3833, 35, 37spcegf 3588 . . . . . . . . 9 (𝐵 ∈ V → (∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → ∃𝑏𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
3915, 32, 38sylc 65 . . . . . . . 8 (𝜑 → ∃𝑏𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
40 nfcv 2974 . . . . . . . . 9 𝑐𝐶
41 nfsbc1v 3789 . . . . . . . . . . 11 𝑐[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
4241nfex 2334 . . . . . . . . . 10 𝑐𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
4342nfex 2334 . . . . . . . . 9 𝑐𝑏𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
44 sbceq1a 3780 . . . . . . . . . 10 (𝑐 = 𝐶 → ((⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ [𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
45442exbidv 1916 . . . . . . . . 9 (𝑐 = 𝐶 → (∃𝑏𝑎(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑏𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
4640, 43, 45spcegf 3588 . . . . . . . 8 (𝐶 ∈ V → (∃𝑏𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → ∃𝑐𝑏𝑎(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
4714, 39, 46sylc 65 . . . . . . 7 (𝜑 → ∃𝑐𝑏𝑎(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
48 excom13 2161 . . . . . . 7 (∃𝑐𝑏𝑎(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑎𝑏𝑐(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
4947, 48sylib 219 . . . . . 6 (𝜑 → ∃𝑎𝑏𝑐(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
50 eqeq1 2822 . . . . . . . 8 (𝑥 = ⟨𝐴, 𝐵, 𝐶⟩ → (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ↔ ⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩))
5150anbi1d 629 . . . . . . 7 (𝑥 = ⟨𝐴, 𝐵, 𝐶⟩ → ((𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ (⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
52513exbidv 1917 . . . . . 6 (𝑥 = ⟨𝐴, 𝐵, 𝐶⟩ → (∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑎𝑏𝑐(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
5349, 52syl5ibrcom 248 . . . . 5 (𝜑 → (𝑥 = ⟨𝐴, 𝐵, 𝐶⟩ → ∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
5413, 53impbid 213 . . . 4 (𝜑 → (∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
5554alrimiv 1919 . . 3 (𝜑 → ∀𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
56 otex 5348 . . . 4 𝐴, 𝐵, 𝐶⟩ ∈ V
57 eqeq2 2830 . . . . . 6 (𝑦 = ⟨𝐴, 𝐵, 𝐶⟩ → (𝑥 = 𝑦𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
5857bibi2d 344 . . . . 5 (𝑦 = ⟨𝐴, 𝐵, 𝐶⟩ → ((∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦) ↔ (∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩)))
5958albidv 1912 . . . 4 (𝑦 = ⟨𝐴, 𝐵, 𝐶⟩ → (∀𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦) ↔ ∀𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩)))
6056, 59spcev 3604 . . 3 (∀𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩) → ∃𝑦𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦))
6155, 60syl 17 . 2 (𝜑 → ∃𝑦𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦))
62 eu6 2652 . 2 (∃!𝑥𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑦𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦))
6361, 62sylibr 235 1 (𝜑 → ∃!𝑥𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079  wal 1526   = wceq 1528  wtru 1529  wex 1771  wcel 2105  ∃!weu 2646  Vcvv 3492  [wsbc 3769  cotp 4565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-ot 4566
This theorem is referenced by:  oeeu  8218
  Copyright terms: Public domain W3C validator