Metamath Proof Explorer

Theorem eueq3

Description: Equality has existential uniqueness (split into 3 cases). (Contributed by NM, 5-Apr-1995) (Proof shortened by Mario Carneiro, 28-Sep-2015)

Ref Expression
Hypotheses eueq3.1 ⊢ A ∈ V
eueq3.2 ⊢ B ∈ V
eueq3.3 ⊢ C ∈ V
eueq3.4 ⊢ ¬ φ ∧ ψ
Assertion eueq3 ⊢ ∃! x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C

Proof

Step Hyp Ref Expression
1 eueq3.1 ⊢ A ∈ V
2 eueq3.2 ⊢ B ∈ V
3 eueq3.3 ⊢ C ∈ V
4 eueq3.4 ⊢ ¬ φ ∧ ψ
5 1 eueqi ⊢ ∃! x x = A
6 ibar ⊢ φ → x = A ↔ φ ∧ x = A
7 pm2.45 ⊢ ¬ φ ∨ ψ → ¬ φ
8 4 imnani ⊢ φ → ¬ ψ
9 8 con2i ⊢ ψ → ¬ φ
10 7 9 jaoi ⊢ ¬ φ ∨ ψ ∨ ψ → ¬ φ
11 10 con2i ⊢ φ → ¬ ¬ φ ∨ ψ ∨ ψ
12 7 con2i ⊢ φ → ¬ ¬ φ ∨ ψ
13 12 bianfd ⊢ φ → ¬ φ ∨ ψ ↔ ¬ φ ∨ ψ ∧ x = B
14 8 bianfd ⊢ φ → ψ ↔ ψ ∧ x = C
15 13 14 orbi12d ⊢ φ → ¬ φ ∨ ψ ∨ ψ ↔ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
16 11 15 mtbid ⊢ φ → ¬ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
17 biorf ⊢ ¬ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C → φ ∧ x = A ↔ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ∨ φ ∧ x = A
18 16 17 syl ⊢ φ → φ ∧ x = A ↔ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ∨ φ ∧ x = A
19 6 18 bitrd ⊢ φ → x = A ↔ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ∨ φ ∧ x = A
20 3orrot ⊢ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ↔ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ∨ φ ∧ x = A
21 df-3or ⊢ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ∨ φ ∧ x = A ↔ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ∨ φ ∧ x = A
22 20 21 bitri ⊢ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ↔ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ∨ φ ∧ x = A
23 19 22 bitr4di ⊢ φ → x = A ↔ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
24 23 eubidv ⊢ φ → ∃! x x = A ↔ ∃! x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
25 5 24 mpbii ⊢ φ → ∃! x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
26 3 eueqi ⊢ ∃! x x = C
27 ibar ⊢ ψ → x = C ↔ ψ ∧ x = C
28 8 adantr ⊢ φ ∧ x = A → ¬ ψ
29 pm2.46 ⊢ ¬ φ ∨ ψ → ¬ ψ
30 29 adantr ⊢ ¬ φ ∨ ψ ∧ x = B → ¬ ψ
31 28 30 jaoi ⊢ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B → ¬ ψ
32 31 con2i ⊢ ψ → ¬ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B
33 biorf ⊢ ¬ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B → ψ ∧ x = C ↔ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
34 32 33 syl ⊢ ψ → ψ ∧ x = C ↔ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
35 27 34 bitrd ⊢ ψ → x = C ↔ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
36 df-3or ⊢ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ↔ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
37 35 36 bitr4di ⊢ ψ → x = C ↔ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
38 37 eubidv ⊢ ψ → ∃! x x = C ↔ ∃! x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
39 26 38 mpbii ⊢ ψ → ∃! x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
40 2 eueqi ⊢ ∃! x x = B
41 ibar ⊢ ¬ φ ∨ ψ → x = B ↔ ¬ φ ∨ ψ ∧ x = B
42 simpl ⊢ φ ∧ x = A → φ
43 simpl ⊢ ψ ∧ x = C → ψ
44 42 43 orim12i ⊢ φ ∧ x = A ∨ ψ ∧ x = C → φ ∨ ψ
45 biorf ⊢ ¬ φ ∧ x = A ∨ ψ ∧ x = C → ¬ φ ∨ ψ ∧ x = B ↔ φ ∧ x = A ∨ ψ ∧ x = C ∨ ¬ φ ∨ ψ ∧ x = B
46 44 45 nsyl5 ⊢ ¬ φ ∨ ψ → ¬ φ ∨ ψ ∧ x = B ↔ φ ∧ x = A ∨ ψ ∧ x = C ∨ ¬ φ ∨ ψ ∧ x = B
47 41 46 bitrd ⊢ ¬ φ ∨ ψ → x = B ↔ φ ∧ x = A ∨ ψ ∧ x = C ∨ ¬ φ ∨ ψ ∧ x = B
48 3orcomb ⊢ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ↔ φ ∧ x = A ∨ ψ ∧ x = C ∨ ¬ φ ∨ ψ ∧ x = B
49 df-3or ⊢ φ ∧ x = A ∨ ψ ∧ x = C ∨ ¬ φ ∨ ψ ∧ x = B ↔ φ ∧ x = A ∨ ψ ∧ x = C ∨ ¬ φ ∨ ψ ∧ x = B
50 48 49 bitri ⊢ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ↔ φ ∧ x = A ∨ ψ ∧ x = C ∨ ¬ φ ∨ ψ ∧ x = B
51 47 50 bitr4di ⊢ ¬ φ ∨ ψ → x = B ↔ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
52 51 eubidv ⊢ ¬ φ ∨ ψ → ∃! x x = B ↔ ∃! x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
53 40 52 mpbii ⊢ ¬ φ ∨ ψ → ∃! x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
54 25 39 53 ecase3 ⊢ ∃! x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C