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

Theorem euotd 5504
Description: Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.)
Hypotheses
Ref Expression
euotd.1 (𝜑𝐴𝑈)
euotd.2 (𝜑𝐵𝑉)
euotd.3 (𝜑𝐶𝑊)
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 476 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶))
3 vex 3470 . . . . . . . . . . . . 13 𝑎 ∈ V
4 vex 3470 . . . . . . . . . . . . 13 𝑏 ∈ V
5 vex 3470 . . . . . . . . . . . . 13 𝑐 ∈ V
63, 4, 5otth 5475 . . . . . . . . . . . 12 (⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝐴, 𝐵, 𝐶⟩ ↔ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶))
72, 6sylibr 233 . . . . . . . . . . 11 ((𝜑𝜓) → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝐴, 𝐵, 𝐶⟩)
87eqeq2d 2735 . . . . . . . . . 10 ((𝜑𝜓) → (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
98biimpd 228 . . . . . . . . 9 ((𝜑𝜓) → (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
109impancom 451 . . . . . . . 8 ((𝜑𝑥 = ⟨𝑎, 𝑏, 𝑐⟩) → (𝜓𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
1110expimpd 453 . . . . . . 7 (𝜑 → ((𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
1211exlimdv 1928 . . . . . 6 (𝜑 → (∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
1312exlimdvv 1929 . . . . 5 (𝜑 → (∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
14 euotd.3 . . . . . . . 8 (𝜑𝐶𝑊)
15 euotd.2 . . . . . . . . 9 (𝜑𝐵𝑉)
16 tru 1537 . . . . . . . . . . 11
17 euotd.1 . . . . . . . . . . . 12 (𝜑𝐴𝑈)
1815adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑎 = 𝐴) → 𝐵𝑉)
1914ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑎 = 𝐴) ∧ 𝑏 = 𝐵) → 𝐶𝑊)
20 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶))
2120, 6sylibr 233 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝐴, 𝐵, 𝐶⟩)
2221eqcomd 2730 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → ⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩)
231biimpar 477 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → 𝜓)
2422, 23jca 511 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → (⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
25 trud 1543 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → ⊤)
2624, 252thd 265 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)) → ((⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
27263anassrs 1357 . . . . . . . . . . . . . 14 ((((𝜑𝑎 = 𝐴) ∧ 𝑏 = 𝐵) ∧ 𝑐 = 𝐶) → ((⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
2819, 27sbcied 3815 . . . . . . . . . . . . 13 (((𝜑𝑎 = 𝐴) ∧ 𝑏 = 𝐵) → ([𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
2918, 28sbcied 3815 . . . . . . . . . . . 12 ((𝜑𝑎 = 𝐴) → ([𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
3017, 29sbcied 3815 . . . . . . . . . . 11 (𝜑 → ([𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ⊤))
3116, 30mpbiri 258 . . . . . . . . . 10 (𝜑[𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
3231spesbcd 3870 . . . . . . . . 9 (𝜑 → ∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
33 nfcv 2895 . . . . . . . . . 10 𝑏𝐵
34 nfsbc1v 3790 . . . . . . . . . . 11 𝑏[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
3534nfex 2309 . . . . . . . . . 10 𝑏𝑎[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
36 sbceq1a 3781 . . . . . . . . . . 11 (𝑏 = 𝐵 → ([𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ [𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
3736exbidv 1916 . . . . . . . . . 10 (𝑏 = 𝐵 → (∃𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
3833, 35, 37spcegf 3574 . . . . . . . . 9 (𝐵𝑉 → (∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → ∃𝑏𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
3915, 32, 38sylc 65 . . . . . . . 8 (𝜑 → ∃𝑏𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
40 nfcv 2895 . . . . . . . . 9 𝑐𝐶
41 nfsbc1v 3790 . . . . . . . . . . 11 𝑐[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
4241nfex 2309 . . . . . . . . . 10 𝑐𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
4342nfex 2309 . . . . . . . . 9 𝑐𝑏𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)
44 sbceq1a 3781 . . . . . . . . . 10 (𝑐 = 𝐶 → ((⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ [𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
45442exbidv 1919 . . . . . . . . 9 (𝑐 = 𝐶 → (∃𝑏𝑎(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑏𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
4640, 43, 45spcegf 3574 . . . . . . . 8 (𝐶𝑊 → (∃𝑏𝑎[𝐶 / 𝑐](⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) → ∃𝑐𝑏𝑎(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
4714, 39, 46sylc 65 . . . . . . 7 (𝜑 → ∃𝑐𝑏𝑎(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
48 excom13 2156 . . . . . . 7 (∃𝑐𝑏𝑎(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑎𝑏𝑐(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
4947, 48sylib 217 . . . . . 6 (𝜑 → ∃𝑎𝑏𝑐(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
50 eqeq1 2728 . . . . . . . 8 (𝑥 = ⟨𝐴, 𝐵, 𝐶⟩ → (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ↔ ⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩))
5150anbi1d 629 . . . . . . 7 (𝑥 = ⟨𝐴, 𝐵, 𝐶⟩ → ((𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ (⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
52513exbidv 1920 . . . . . 6 (𝑥 = ⟨𝐴, 𝐵, 𝐶⟩ → (∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑎𝑏𝑐(⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
5349, 52syl5ibrcom 246 . . . . 5 (𝜑 → (𝑥 = ⟨𝐴, 𝐵, 𝐶⟩ → ∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓)))
5413, 53impbid 211 . . . 4 (𝜑 → (∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
5554alrimiv 1922 . . 3 (𝜑 → ∀𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
56 otex 5456 . . . 4 𝐴, 𝐵, 𝐶⟩ ∈ V
57 eqeq2 2736 . . . . . 6 (𝑦 = ⟨𝐴, 𝐵, 𝐶⟩ → (𝑥 = 𝑦𝑥 = ⟨𝐴, 𝐵, 𝐶⟩))
5857bibi2d 342 . . . . 5 (𝑦 = ⟨𝐴, 𝐵, 𝐶⟩ → ((∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦) ↔ (∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩)))
5958albidv 1915 . . . 4 (𝑦 = ⟨𝐴, 𝐵, 𝐶⟩ → (∀𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦) ↔ ∀𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩)))
6056, 59spcev 3588 . . 3 (∀𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = ⟨𝐴, 𝐵, 𝐶⟩) → ∃𝑦𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦))
6155, 60syl 17 . 2 (𝜑 → ∃𝑦𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦))
62 eu6 2560 . 2 (∃!𝑥𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ ∃𝑦𝑥(∃𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓) ↔ 𝑥 = 𝑦))
6361, 62sylibr 233 1 (𝜑 → ∃!𝑥𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084  wal 1531   = wceq 1533  wtru 1534  wex 1773  wcel 2098  ∃!weu 2554  [wsbc 3770  cotp 4629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3771  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-ot 4630
This theorem is referenced by:  oeeu  8599
  Copyright terms: Public domain W3C validator