Theorem eueq3 3011

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	⊢ A ∈ V
eueq3.2	⊢ B ∈ V
eueq3.3	⊢ C ∈ V
eueq3.4	⊢ ¬ (φ ∧ ψ)

Assertion

Ref	Expression
eueq3	⊢ ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))

Distinct variable groups:   φ,x   ψ,x   x,A   x,B   x,C

Proof of Theorem eueq3

Step	Hyp	Ref	Expression
1		eueq3.1	. . . 4 ⊢ A ∈ V
2	1	eueq1 3009	. . 3 ⊢ ∃!x x = A
3		ibar 490	. . . . . 6 ⊢ (φ → (x = A ↔ (φ ∧ x = A)))
4		pm2.45 386	. . . . . . . . . 10 ⊢ (¬ (φ ∨ ψ) → ¬ φ)
5		eueq3.4	. . . . . . . . . . . 12 ⊢ ¬ (φ ∧ ψ)
6	5	imnani 412	. . . . . . . . . . 11 ⊢ (φ → ¬ ψ)
7	6	con2i 112	. . . . . . . . . 10 ⊢ (ψ → ¬ φ)
8	4, 7	jaoi 368	. . . . . . . . 9 ⊢ ((¬ (φ ∨ ψ) ∨ ψ) → ¬ φ)
9	8	con2i 112	. . . . . . . 8 ⊢ (φ → ¬ (¬ (φ ∨ ψ) ∨ ψ))
10	4	con2i 112	. . . . . . . . . 10 ⊢ (φ → ¬ ¬ (φ ∨ ψ))
11	10	bianfd 892	. . . . . . . . 9 ⊢ (φ → (¬ (φ ∨ ψ) ↔ (¬ (φ ∨ ψ) ∧ x = B)))
12	6	bianfd 892	. . . . . . . . 9 ⊢ (φ → (ψ ↔ (ψ ∧ x = C)))
13	11, 12	orbi12d 690	. . . . . . . 8 ⊢ (φ → ((¬ (φ ∨ ψ) ∨ ψ) ↔ ((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
14	9, 13	mtbid 291	. . . . . . 7 ⊢ (φ → ¬ ((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)))
15		biorf 394	. . . . . . 7 ⊢ (¬ ((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) → ((φ ∧ x = A) ↔ (((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) ∨ (φ ∧ x = A))))
16	14, 15	syl 15	. . . . . 6 ⊢ (φ → ((φ ∧ x = A) ↔ (((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) ∨ (φ ∧ x = A))))
17	3, 16	bitrd 244	. . . . 5 ⊢ (φ → (x = A ↔ (((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) ∨ (φ ∧ x = A))))
18		3orrot 940	. . . . . 6 ⊢ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) ↔ ((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C) ∨ (φ ∧ x = A)))
19		df-3or 935	. . . . . 6 ⊢ (((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C) ∨ (φ ∧ x = A)) ↔ (((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) ∨ (φ ∧ x = A)))
20	18, 19	bitri 240	. . . . 5 ⊢ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) ↔ (((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) ∨ (φ ∧ x = A)))
21	17, 20	syl6bbr 254	. . . 4 ⊢ (φ → (x = A ↔ ((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
22	21	eubidv 2212	. . 3 ⊢ (φ → (∃!x x = A ↔ ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
23	2, 22	mpbii 202	. 2 ⊢ (φ → ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)))
24		eueq3.3	. . . 4 ⊢ C ∈ V
25	24	eueq1 3009	. . 3 ⊢ ∃!x x = C
26		ibar 490	. . . . . 6 ⊢ (ψ → (x = C ↔ (ψ ∧ x = C)))
27	6	adantr 451	. . . . . . . . 9 ⊢ ((φ ∧ x = A) → ¬ ψ)
28		pm2.46 387	. . . . . . . . . 10 ⊢ (¬ (φ ∨ ψ) → ¬ ψ)
29	28	adantr 451	. . . . . . . . 9 ⊢ ((¬ (φ ∨ ψ) ∧ x = B) → ¬ ψ)
30	27, 29	jaoi 368	. . . . . . . 8 ⊢ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B)) → ¬ ψ)
31	30	con2i 112	. . . . . . 7 ⊢ (ψ → ¬ ((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B)))
32		biorf 394	. . . . . . 7 ⊢ (¬ ((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B)) → ((ψ ∧ x = C) ↔ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B)) ∨ (ψ ∧ x = C))))
33	31, 32	syl 15	. . . . . 6 ⊢ (ψ → ((ψ ∧ x = C) ↔ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B)) ∨ (ψ ∧ x = C))))
34	26, 33	bitrd 244	. . . . 5 ⊢ (ψ → (x = C ↔ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B)) ∨ (ψ ∧ x = C))))
35		df-3or 935	. . . . 5 ⊢ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) ↔ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B)) ∨ (ψ ∧ x = C)))
36	34, 35	syl6bbr 254	. . . 4 ⊢ (ψ → (x = C ↔ ((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
37	36	eubidv 2212	. . 3 ⊢ (ψ → (∃!x x = C ↔ ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
38	25, 37	mpbii 202	. 2 ⊢ (ψ → ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)))
39		eueq3.2	. . . 4 ⊢ B ∈ V
40	39	eueq1 3009	. . 3 ⊢ ∃!x x = B
41		ibar 490	. . . . . 6 ⊢ (¬ (φ ∨ ψ) → (x = B ↔ (¬ (φ ∨ ψ) ∧ x = B)))
42		simpl 443	. . . . . . . . 9 ⊢ ((φ ∧ x = A) → φ)
43		simpl 443	. . . . . . . . 9 ⊢ ((ψ ∧ x = C) → ψ)
44	42, 43	orim12i 502	. . . . . . . 8 ⊢ (((φ ∧ x = A) ∨ (ψ ∧ x = C)) → (φ ∨ ψ))
45	44	con3i 127	. . . . . . 7 ⊢ (¬ (φ ∨ ψ) → ¬ ((φ ∧ x = A) ∨ (ψ ∧ x = C)))
46		biorf 394	. . . . . . 7 ⊢ (¬ ((φ ∧ x = A) ∨ (ψ ∧ x = C)) → ((¬ (φ ∨ ψ) ∧ x = B) ↔ (((φ ∧ x = A) ∨ (ψ ∧ x = C)) ∨ (¬ (φ ∨ ψ) ∧ x = B))))
47	45, 46	syl 15	. . . . . 6 ⊢ (¬ (φ ∨ ψ) → ((¬ (φ ∨ ψ) ∧ x = B) ↔ (((φ ∧ x = A) ∨ (ψ ∧ x = C)) ∨ (¬ (φ ∨ ψ) ∧ x = B))))
48	41, 47	bitrd 244	. . . . 5 ⊢ (¬ (φ ∨ ψ) → (x = B ↔ (((φ ∧ x = A) ∨ (ψ ∧ x = C)) ∨ (¬ (φ ∨ ψ) ∧ x = B))))
49		3orcomb 944	. . . . . 6 ⊢ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) ↔ ((φ ∧ x = A) ∨ (ψ ∧ x = C) ∨ (¬ (φ ∨ ψ) ∧ x = B)))
50		df-3or 935	. . . . . 6 ⊢ (((φ ∧ x = A) ∨ (ψ ∧ x = C) ∨ (¬ (φ ∨ ψ) ∧ x = B)) ↔ (((φ ∧ x = A) ∨ (ψ ∧ x = C)) ∨ (¬ (φ ∨ ψ) ∧ x = B)))
51	49, 50	bitri 240	. . . . 5 ⊢ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) ↔ (((φ ∧ x = A) ∨ (ψ ∧ x = C)) ∨ (¬ (φ ∨ ψ) ∧ x = B)))
52	48, 51	syl6bbr 254	. . . 4 ⊢ (¬ (φ ∨ ψ) → (x = B ↔ ((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
53	52	eubidv 2212	. . 3 ⊢ (¬ (φ ∨ ψ) → (∃!x x = B ↔ ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
54	40, 53	mpbii 202	. 2 ⊢ (¬ (φ ∨ ψ) → ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)))
55	23, 38, 54	ecase3 907	1 ⊢ ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))

Syntax hints:  ¬ wn 3   ↔ wb 176   ∨ wo 357   ∧ wa 358   ∨ w3o 933   = wceq 1642   ∈ wcel 1710  ∃!weu 2204  Vcvv 2859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2861

This theorem is referenced by:  moeq3  3013