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

Theorem eueq3 3348
 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 3346 . . 3 ∃!𝑥 𝑥 = 𝐴
3 ibar 524 . . . . . 6 (𝜑 → (𝑥 = 𝐴 ↔ (𝜑𝑥 = 𝐴)))
4 pm2.45 411 . . . . . . . . . 10 (¬ (𝜑𝜓) → ¬ 𝜑)
5 eueq3.4 . . . . . . . . . . . 12 ¬ (𝜑𝜓)
65imnani 438 . . . . . . . . . . 11 (𝜑 → ¬ 𝜓)
76con2i 133 . . . . . . . . . 10 (𝜓 → ¬ 𝜑)
84, 7jaoi 393 . . . . . . . . 9 ((¬ (𝜑𝜓) ∨ 𝜓) → ¬ 𝜑)
98con2i 133 . . . . . . . 8 (𝜑 → ¬ (¬ (𝜑𝜓) ∨ 𝜓))
104con2i 133 . . . . . . . . . 10 (𝜑 → ¬ ¬ (𝜑𝜓))
1110bianfd 963 . . . . . . . . 9 (𝜑 → (¬ (𝜑𝜓) ↔ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
126bianfd 963 . . . . . . . . 9 (𝜑 → (𝜓 ↔ (𝜓𝑥 = 𝐶)))
1311, 12orbi12d 742 . . . . . . . 8 (𝜑 → ((¬ (𝜑𝜓) ∨ 𝜓) ↔ ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
149, 13mtbid 313 . . . . . . 7 (𝜑 → ¬ ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)))
15 biorf 419 . . . . . . 7 (¬ ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) → ((𝜑𝑥 = 𝐴) ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴))))
1614, 15syl 17 . . . . . 6 (𝜑 → ((𝜑𝑥 = 𝐴) ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴))))
173, 16bitrd 267 . . . . 5 (𝜑 → (𝑥 = 𝐴 ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴))))
18 3orrot 1037 . . . . . 6 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶) ∨ (𝜑𝑥 = 𝐴)))
19 df-3or 1032 . . . . . 6 (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶) ∨ (𝜑𝑥 = 𝐴)) ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴)))
2018, 19bitri 263 . . . . 5 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴)))
2117, 20syl6bbr 277 . . . 4 (𝜑 → (𝑥 = 𝐴 ↔ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
2221eubidv 2478 . . 3 (𝜑 → (∃!𝑥 𝑥 = 𝐴 ↔ ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
232, 22mpbii 222 . 2 (𝜑 → ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)))
24 eueq3.3 . . . 4 𝐶 ∈ V
2524eueq1 3346 . . 3 ∃!𝑥 𝑥 = 𝐶
26 ibar 524 . . . . . 6 (𝜓 → (𝑥 = 𝐶 ↔ (𝜓𝑥 = 𝐶)))
276adantr 480 . . . . . . . . 9 ((𝜑𝑥 = 𝐴) → ¬ 𝜓)
28 pm2.46 412 . . . . . . . . . 10 (¬ (𝜑𝜓) → ¬ 𝜓)
2928adantr 480 . . . . . . . . 9 ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) → ¬ 𝜓)
3027, 29jaoi 393 . . . . . . . 8 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) → ¬ 𝜓)
3130con2i 133 . . . . . . 7 (𝜓 → ¬ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
32 biorf 419 . . . . . . 7 (¬ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) → ((𝜓𝑥 = 𝐶) ↔ (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓𝑥 = 𝐶))))
3331, 32syl 17 . . . . . 6 (𝜓 → ((𝜓𝑥 = 𝐶) ↔ (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓𝑥 = 𝐶))))
3426, 33bitrd 267 . . . . 5 (𝜓 → (𝑥 = 𝐶 ↔ (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓𝑥 = 𝐶))))
35 df-3or 1032 . . . . 5 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓𝑥 = 𝐶)))
3634, 35syl6bbr 277 . . . 4 (𝜓 → (𝑥 = 𝐶 ↔ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
3736eubidv 2478 . . 3 (𝜓 → (∃!𝑥 𝑥 = 𝐶 ↔ ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
3825, 37mpbii 222 . 2 (𝜓 → ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)))
39 eueq3.2 . . . 4 𝐵 ∈ V
4039eueq1 3346 . . 3 ∃!𝑥 𝑥 = 𝐵
41 ibar 524 . . . . . 6 (¬ (𝜑𝜓) → (𝑥 = 𝐵 ↔ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
42 simpl 472 . . . . . . . . 9 ((𝜑𝑥 = 𝐴) → 𝜑)
43 simpl 472 . . . . . . . . 9 ((𝜓𝑥 = 𝐶) → 𝜓)
4442, 43orim12i 537 . . . . . . . 8 (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) → (𝜑𝜓))
4544con3i 149 . . . . . . 7 (¬ (𝜑𝜓) → ¬ ((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)))
46 biorf 419 . . . . . . 7 (¬ ((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) → ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵))))
4745, 46syl 17 . . . . . 6 (¬ (𝜑𝜓) → ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵))))
4841, 47bitrd 267 . . . . 5 (¬ (𝜑𝜓) → (𝑥 = 𝐵 ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵))))
49 3orcomb 1041 . . . . . 6 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ ((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
50 df-3or 1032 . . . . . 6 (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
5149, 50bitri 263 . . . . 5 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
5248, 51syl6bbr 277 . . . 4 (¬ (𝜑𝜓) → (𝑥 = 𝐵 ↔ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
5352eubidv 2478 . . 3 (¬ (𝜑𝜓) → (∃!𝑥 𝑥 = 𝐵 ↔ ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
5440, 53mpbii 222 . 2 (¬ (𝜑𝜓) → ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)))
5523, 38, 54ecase3 979 1 ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977  ∃!weu 2458  Vcvv 3173 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175 This theorem is referenced by:  moeq3  3350
 Copyright terms: Public domain W3C validator