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

Theorem eueq3 3653
 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
21eueqi 3651 . . 3 ∃!𝑥 𝑥 = 𝐴
3 ibar 532 . . . . . 6 (𝜑 → (𝑥 = 𝐴 ↔ (𝜑𝑥 = 𝐴)))
4 pm2.45 879 . . . . . . . . . 10 (¬ (𝜑𝜓) → ¬ 𝜑)
5 eueq3.4 . . . . . . . . . . . 12 ¬ (𝜑𝜓)
65imnani 404 . . . . . . . . . . 11 (𝜑 → ¬ 𝜓)
76con2i 141 . . . . . . . . . 10 (𝜓 → ¬ 𝜑)
84, 7jaoi 854 . . . . . . . . 9 ((¬ (𝜑𝜓) ∨ 𝜓) → ¬ 𝜑)
98con2i 141 . . . . . . . 8 (𝜑 → ¬ (¬ (𝜑𝜓) ∨ 𝜓))
104con2i 141 . . . . . . . . . 10 (𝜑 → ¬ ¬ (𝜑𝜓))
1110bianfd 538 . . . . . . . . 9 (𝜑 → (¬ (𝜑𝜓) ↔ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
126bianfd 538 . . . . . . . . 9 (𝜑 → (𝜓 ↔ (𝜓𝑥 = 𝐶)))
1311, 12orbi12d 916 . . . . . . . 8 (𝜑 → ((¬ (𝜑𝜓) ∨ 𝜓) ↔ ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
149, 13mtbid 327 . . . . . . 7 (𝜑 → ¬ ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)))
15 biorf 934 . . . . . . 7 (¬ ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) → ((𝜑𝑥 = 𝐴) ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴))))
1614, 15syl 17 . . . . . 6 (𝜑 → ((𝜑𝑥 = 𝐴) ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴))))
173, 16bitrd 282 . . . . 5 (𝜑 → (𝑥 = 𝐴 ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴))))
18 3orrot 1089 . . . . . 6 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶) ∨ (𝜑𝑥 = 𝐴)))
19 df-3or 1085 . . . . . 6 (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶) ∨ (𝜑𝑥 = 𝐴)) ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴)))
2018, 19bitri 278 . . . . 5 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ (((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ∨ (𝜑𝑥 = 𝐴)))
2117, 20syl6bbr 292 . . . 4 (𝜑 → (𝑥 = 𝐴 ↔ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
2221eubidv 2650 . . 3 (𝜑 → (∃!𝑥 𝑥 = 𝐴 ↔ ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
232, 22mpbii 236 . 2 (𝜑 → ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)))
24 eueq3.3 . . . 4 𝐶 ∈ V
2524eueqi 3651 . . 3 ∃!𝑥 𝑥 = 𝐶
26 ibar 532 . . . . . 6 (𝜓 → (𝑥 = 𝐶 ↔ (𝜓𝑥 = 𝐶)))
276adantr 484 . . . . . . . . 9 ((𝜑𝑥 = 𝐴) → ¬ 𝜓)
28 pm2.46 880 . . . . . . . . . 10 (¬ (𝜑𝜓) → ¬ 𝜓)
2928adantr 484 . . . . . . . . 9 ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) → ¬ 𝜓)
3027, 29jaoi 854 . . . . . . . 8 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) → ¬ 𝜓)
3130con2i 141 . . . . . . 7 (𝜓 → ¬ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
32 biorf 934 . . . . . . 7 (¬ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) → ((𝜓𝑥 = 𝐶) ↔ (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓𝑥 = 𝐶))))
3331, 32syl 17 . . . . . 6 (𝜓 → ((𝜓𝑥 = 𝐶) ↔ (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓𝑥 = 𝐶))))
3426, 33bitrd 282 . . . . 5 (𝜓 → (𝑥 = 𝐶 ↔ (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓𝑥 = 𝐶))))
35 df-3or 1085 . . . . 5 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓𝑥 = 𝐶)))
3634, 35syl6bbr 292 . . . 4 (𝜓 → (𝑥 = 𝐶 ↔ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
3736eubidv 2650 . . 3 (𝜓 → (∃!𝑥 𝑥 = 𝐶 ↔ ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
3825, 37mpbii 236 . 2 (𝜓 → ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)))
39 eueq3.2 . . . 4 𝐵 ∈ V
4039eueqi 3651 . . 3 ∃!𝑥 𝑥 = 𝐵
41 ibar 532 . . . . . 6 (¬ (𝜑𝜓) → (𝑥 = 𝐵 ↔ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
42 simpl 486 . . . . . . . 8 ((𝜑𝑥 = 𝐴) → 𝜑)
43 simpl 486 . . . . . . . 8 ((𝜓𝑥 = 𝐶) → 𝜓)
4442, 43orim12i 906 . . . . . . 7 (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) → (𝜑𝜓))
45 biorf 934 . . . . . . 7 (¬ ((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) → ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵))))
4644, 45nsyl5 162 . . . . . 6 (¬ (𝜑𝜓) → ((¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵))))
4741, 46bitrd 282 . . . . 5 (¬ (𝜑𝜓) → (𝑥 = 𝐵 ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵))))
48 3orcomb 1091 . . . . . 6 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ ((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
49 df-3or 1085 . . . . . 6 (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)) ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
5048, 49bitri 278 . . . . 5 (((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)) ↔ (((𝜑𝑥 = 𝐴) ∨ (𝜓𝑥 = 𝐶)) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵)))
5147, 50syl6bbr 292 . . . 4 (¬ (𝜑𝜓) → (𝑥 = 𝐵 ↔ ((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
5251eubidv 2650 . . 3 (¬ (𝜑𝜓) → (∃!𝑥 𝑥 = 𝐵 ↔ ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))
5340, 52mpbii 236 . 2 (¬ (𝜑𝜓) → ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶)))
5423, 38, 53ecase3 1028 1 ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∨ w3o 1083   = wceq 1538   ∈ wcel 2112  ∃!weu 2631  Vcvv 3444 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-ex 1782  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446 This theorem is referenced by:  moeq3  3654
 Copyright terms: Public domain W3C validator