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

Theorem eueq3 3368
Description: Equality has existential uniqueness (split into 3 cases). (Contributed by NM, 5-Apr-1995.) (Proof shortened by Mario Carneiro, 28-Sep-2015.)
Hypotheses
Ref Expression
eueq3.1 𝐴 ∈ V
eueq3.2 𝐵 ∈ V
eueq3.3 𝐶 ∈ V
eueq3.4 ¬ (𝜑𝜓)
Assertion
Ref Expression
eueq3 ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))
Distinct variable groups:   𝜑,𝑥   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶

Proof of Theorem eueq3
StepHypRef Expression
1 eueq3.1 . . . 4 𝐴 ∈ V
21eueq1 3366 . . 3 ∃!𝑥 𝑥 = 𝐴
3 ibar 525 . . . . . 6 (𝜑 → (𝑥 = 𝐴 ↔ (𝜑𝑥 = 𝐴)))
4 pm2.45 412 . . . . . . . . . 10 (¬ (𝜑𝜓) → ¬ 𝜑)
5 eueq3.4 . . . . . . . . . . . 12 ¬ (𝜑𝜓)
65imnani 439 . . . . . . . . . . 11 (𝜑 → ¬ 𝜓)
76con2i 134 . . . . . . . . . 10 (𝜓 → ¬ 𝜑)
84, 7jaoi 394 . . . . . . . . 9 ((¬ (𝜑𝜓) ∨ 𝜓) → ¬ 𝜑)
98con2i 134 . . . . . . . 8 (𝜑 → ¬ (¬ (𝜑𝜓) ∨ 𝜓))
104con2i 134 . . . . . . . . . 10 (𝜑 → ¬ ¬ (𝜑𝜓))
1110bianfd 966 . . . . . . . . 9 (𝜑 → (¬ (𝜑𝜓) ↔ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
126bianfd 966 . . . . . . . . 9 (𝜑 → (𝜓 ↔ (𝜓𝑥 = 𝐶)))
1311, 12orbi12d 745 . . . . . . . 8 (𝜑 → ((¬ (𝜑𝜓) ∨ 𝜓) ↔ ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
149, 13mtbid 314 . . . . . . 7 (𝜑 → ¬ ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)))
15 biorf 420 . . . . . . 7 (¬ ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) → ((𝜑𝑥 = 𝐴) ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴))))
1614, 15syl 17 . . . . . 6 (𝜑 → ((𝜑𝑥 = 𝐴) ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴))))
173, 16bitrd 268 . . . . 5 (𝜑 → (𝑥 = 𝐴 ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴))))
18 3orrot 1042 . . . . . 6 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶) ∨ (𝜑𝑥 = 𝐴)))
19 df-3or 1037 . . . . . 6 (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶) ∨ (𝜑𝑥 = 𝐴)) ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴)))
2018, 19bitri 264 . . . . 5 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴)))
2117, 20syl6bbr 278 . . . 4 (𝜑 → (𝑥 = 𝐴 ↔ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
2221eubidv 2494 . . 3 (𝜑 → (∃!𝑥 𝑥 = 𝐴 ↔ ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
232, 22mpbii 223 . 2 (𝜑 → ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)))
24 eueq3.3 . . . 4 𝐶 ∈ V
2524eueq1 3366 . . 3 ∃!𝑥 𝑥 = 𝐶
26 ibar 525 . . . . . 6 (𝜓 → (𝑥 = 𝐶 ↔ (𝜓𝑥 = 𝐶)))
276adantr 481 . . . . . . . . 9 ((𝜑𝑥 = 𝐴) → ¬ 𝜓)
28 pm2.46 413 . . . . . . . . . 10 (¬ (𝜑𝜓) → ¬ 𝜓)
2928adantr 481 . . . . . . . . 9 ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) → ¬ 𝜓)
3027, 29jaoi 394 . . . . . . . 8 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) → ¬ 𝜓)
3130con2i 134 . . . . . . 7 (𝜓 → ¬ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
32 biorf 420 . . . . . . 7 (¬ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) → ((𝜓𝑥 = 𝐶) ↔ (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓𝑥 = 𝐶))))
3331, 32syl 17 . . . . . 6 (𝜓 → ((𝜓𝑥 = 𝐶) ↔ (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓𝑥 = 𝐶))))
3426, 33bitrd 268 . . . . 5 (𝜓 → (𝑥 = 𝐶 ↔ (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓𝑥 = 𝐶))))
35 df-3or 1037 . . . . 5 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓𝑥 = 𝐶)))
3634, 35syl6bbr 278 . . . 4 (𝜓 → (𝑥 = 𝐶 ↔ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
3736eubidv 2494 . . 3 (𝜓 → (∃!𝑥 𝑥 = 𝐶 ↔ ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
3825, 37mpbii 223 . 2 (𝜓 → ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)))
39 eueq3.2 . . . 4 𝐵 ∈ V
4039eueq1 3366 . . 3 ∃!𝑥 𝑥 = 𝐵
41 ibar 525 . . . . . 6 (¬ (𝜑𝜓) → (𝑥 = 𝐵 ↔ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
42 simpl 473 . . . . . . . . 9 ((𝜑𝑥 = 𝐴) → 𝜑)
43 simpl 473 . . . . . . . . 9 ((𝜓𝑥 = 𝐶) → 𝜓)
4442, 43orim12i 538 . . . . . . . 8 (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) → (𝜑𝜓))
4544con3i 150 . . . . . . 7 (¬ (𝜑𝜓) → ¬ ((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)))
46 biorf 420 . . . . . . 7 (¬ ((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) → ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵))))
4745, 46syl 17 . . . . . 6 (¬ (𝜑𝜓) → ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵))))
4841, 47bitrd 268 . . . . 5 (¬ (𝜑𝜓) → (𝑥 = 𝐵 ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵))))
49 3orcomb 1046 . . . . . 6 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ ((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
50 df-3or 1037 . . . . . 6 (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
5149, 50bitri 264 . . . . 5 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
5248, 51syl6bbr 278 . . . 4 (¬ (𝜑𝜓) → (𝑥 = 𝐵 ↔ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
5352eubidv 2494 . . 3 (¬ (𝜑𝜓) → (∃!𝑥 𝑥 = 𝐵 ↔ ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
5440, 53mpbii 223 . 2 (¬ (𝜑𝜓) → ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)))
5523, 38, 54ecase3 981 1 ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wo 383  wa 384  w3o 1035   = wceq 1480  wcel 1992  ∃!weu 2474  Vcvv 3191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-v 3193
This theorem is referenced by:  moeq3  3370
  Copyright terms: Public domain W3C validator