This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ V
eueq3.2 ⊢ 𝐵 ∈ V
eueq3.3 ⊢ 𝐶 ∈ V
eueq3.4 ⊢ ¬ ( 𝜑 ∧ 𝜓 )
Assertion eueq3 ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ ( 𝜑 ∨ 𝜓 ) ∧ 𝑥 = 𝐵 ) ∨ ( 𝜓 ∧ 𝑥 = 𝐶 ) )

Proof

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