Theorem eueq3 1430

Description: Equality has existential uniqueness (split into 3 cases).

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 group(s):   φ,x   ψ,x   x,A   x,B   x,C

Proof of Theorem eueq3

Step	Hyp	Ref	Expression
1		euorv 1025	. . . 4 ⊢ ((¬ (¬ (φ ∨ ψ) ∨ ψ) ∧ ∃!x(φ ∧ x = A)) → ∃!x((¬ (φ ∨ ψ) ∨ ψ) ∨ (φ ∧ x = A)))
2		pm2.45 228	. . . . . 6 ⊢ (¬ (φ ∨ ψ) → ¬ φ)
3		eueq3.4	. . . . . . . 8 ⊢ ¬ (φ ∧ ψ)
4		imnan 207	. . . . . . . 8 ⊢ ((φ → ¬ ψ) ↔ ¬ (φ ∧ ψ))
5	3, 4	mpbir 165	. . . . . . 7 ⊢ (φ → ¬ ψ)
6	5	con2i 89	. . . . . 6 ⊢ (ψ → ¬ φ)
7	2, 6	jaoi 275	. . . . 5 ⊢ ((¬ (φ ∨ ψ) ∨ ψ) → ¬ φ)
8	7	con2i 89	. . . 4 ⊢ (φ → ¬ (¬ (φ ∨ ψ) ∨ ψ))
9		eueq3.1	. . . . . 6 ⊢ A ∈ V
10	9	eueq1 1428	. . . . 5 ⊢ ∃!x x = A
11		euanv 1053	. . . . . 6 ⊢ (∃!x(φ ∧ x = A) ↔ (φ ∧ ∃!x x = A))
12	11	biimpr 134	. . . . 5 ⊢ ((φ ∧ ∃!x x = A) → ∃!x(φ ∧ x = A))
13	10, 12	mpan2 519	. . . 4 ⊢ (φ → ∃!x(φ ∧ x = A))
14	1, 8, 13	sylanc 361	. . 3 ⊢ (φ → ∃!x((¬ (φ ∨ ψ) ∨ ψ) ∨ (φ ∧ x = A)))
15		negb 79	. . . . . . . . 9 ⊢ ((φ ∨ ψ) → ¬ ¬ (φ ∨ ψ))
16	15	orci 226	. . . . . . . 8 ⊢ (φ → ¬ ¬ (φ ∨ ψ))
17	16	bianfd 554	. . . . . . 7 ⊢ (φ → (¬ (φ ∨ ψ) ↔ (¬ (φ ∨ ψ) ∧ x = B)))
18	5	bianfd 554	. . . . . . 7 ⊢ (φ → (ψ ↔ (ψ ∧ x = C)))
19	17, 18	orbi12d 475	. . . . . 6 ⊢ (φ → ((¬ (φ ∨ ψ) ∨ ψ) ↔ ((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
20	19	orbi2d 466	. . . . 5 ⊢ (φ → (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∨ ψ)) ↔ ((φ ∧ x = A) ∨ ((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)))))
21		orcom 209	. . . . 5 ⊢ (((¬ (φ ∨ ψ) ∨ ψ) ∨ (φ ∧ x = A)) ↔ ((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∨ ψ)))
22		3orass 584	. . . . 5 ⊢ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) ↔ ((φ ∧ x = A) ∨ ((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
23	20, 21, 22	3bitr4g 428	. . . 4 ⊢ (φ → (((¬ (φ ∨ ψ) ∨ ψ) ∨ (φ ∧ x = A)) ↔ ((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
24	23	bieudv 1013	. . 3 ⊢ (φ → (∃!x((¬ (φ ∨ ψ) ∨ ψ) ∨ (φ ∧ x = A)) ↔ ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
25	14, 24	mpbid 170	. 2 ⊢ (φ → ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)))
26		euorv 1025	. . . 4 ⊢ ((¬ (φ ∨ ¬ (φ ∨ ψ)) ∧ ∃!x(ψ ∧ x = C)) → ∃!x((φ ∨ ¬ (φ ∨ ψ)) ∨ (ψ ∧ x = C)))
27		pm2.46 229	. . . . . 6 ⊢ (¬ (φ ∨ ψ) → ¬ ψ)
28	5, 27	jaoi 275	. . . . 5 ⊢ ((φ ∨ ¬ (φ ∨ ψ)) → ¬ ψ)
29	28	con2i 89	. . . 4 ⊢ (ψ → ¬ (φ ∨ ¬ (φ ∨ ψ)))
30		eueq3.3	. . . . . 6 ⊢ C ∈ V
31	30	eueq1 1428	. . . . 5 ⊢ ∃!x x = C
32		euanv 1053	. . . . . 6 ⊢ (∃!x(ψ ∧ x = C) ↔ (ψ ∧ ∃!x x = C))
33	32	biimpr 134	. . . . 5 ⊢ ((ψ ∧ ∃!x x = C) → ∃!x(ψ ∧ x = C))
34	31, 33	mpan2 519	. . . 4 ⊢ (ψ → ∃!x(ψ ∧ x = C))
35	26, 29, 34	sylanc 361	. . 3 ⊢ (ψ → ∃!x((φ ∨ ¬ (φ ∨ ψ)) ∨ (ψ ∧ x = C)))
36	6	bianfd 554	. . . . . . 7 ⊢ (ψ → (φ ↔ (φ ∧ x = A)))
37	15	olci 227	. . . . . . . 8 ⊢ (ψ → ¬ ¬ (φ ∨ ψ))
38	37	bianfd 554	. . . . . . 7 ⊢ (ψ → (¬ (φ ∨ ψ) ↔ (¬ (φ ∨ ψ) ∧ x = B)))
39	36, 38	orbi12d 475	. . . . . 6 ⊢ (ψ → ((φ ∨ ¬ (φ ∨ ψ)) ↔ ((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B))))
40	39	orbi1d 467	. . . . 5 ⊢ (ψ → (((φ ∨ ¬ (φ ∨ ψ)) ∨ (ψ ∧ x = C)) ↔ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B)) ∨ (ψ ∧ x = C))))
41		df-3or 582	. . . . 5 ⊢ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)) ↔ (((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B)) ∨ (ψ ∧ x = C)))
42	40, 41	syl6bbr 416	. . . 4 ⊢ (ψ → (((φ ∨ ¬ (φ ∨ ψ)) ∨ (ψ ∧ x = C)) ↔ ((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
43	42	bieudv 1013	. . 3 ⊢ (ψ → (∃!x((φ ∨ ¬ (φ ∨ ψ)) ∨ (ψ ∧ x = C)) ↔ ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
44	35, 43	mpbid 170	. 2 ⊢ (ψ → ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)))
45		eueq3.2	. . . . . 6 ⊢ B ∈ V
46	45	eueq1 1428	. . . . 5 ⊢ ∃!x x = B
47		euanv 1053	. . . . . 6 ⊢ (∃!x(¬ (φ ∨ ψ) ∧ x = B) ↔ (¬ (φ ∨ ψ) ∧ ∃!x x = B))
48	47	biimpr 134	. . . . 5 ⊢ ((¬ (φ ∨ ψ) ∧ ∃!x x = B) → ∃!x(¬ (φ ∨ ψ) ∧ x = B))
49	46, 48	mpan2 519	. . . 4 ⊢ (¬ (φ ∨ ψ) → ∃!x(¬ (φ ∨ ψ) ∧ x = B))
50		euorv 1025	. . . 4 ⊢ ((¬ (φ ∨ ψ) ∧ ∃!x(¬ (φ ∨ ψ) ∧ x = B)) → ∃!x((φ ∨ ψ) ∨ (¬ (φ ∨ ψ) ∧ x = B)))
51	49, 50	mpdan 527	. . 3 ⊢ (¬ (φ ∨ ψ) → ∃!x((φ ∨ ψ) ∨ (¬ (φ ∨ ψ) ∧ x = B)))
52	2	bianfd 554	. . . . . 6 ⊢ (¬ (φ ∨ ψ) → (φ ↔ (φ ∧ x = A)))
53	27	bianfd 554	. . . . . . . 8 ⊢ (¬ (φ ∨ ψ) → (ψ ↔ (ψ ∧ x = C)))
54	53	orbi1d 467	. . . . . . 7 ⊢ (¬ (φ ∨ ψ) → ((ψ ∨ (¬ (φ ∨ ψ) ∧ x = B)) ↔ ((ψ ∧ x = C) ∨ (¬ (φ ∨ ψ) ∧ x = B))))
55		orcom 209	. . . . . . 7 ⊢ (((ψ ∧ x = C) ∨ (¬ (φ ∨ ψ) ∧ x = B)) ↔ ((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)))
56	54, 55	syl6bb 414	. . . . . 6 ⊢ (¬ (φ ∨ ψ) → ((ψ ∨ (¬ (φ ∨ ψ) ∧ x = B)) ↔ ((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
57	52, 56	orbi12d 475	. . . . 5 ⊢ (¬ (φ ∨ ψ) → ((φ ∨ (ψ ∨ (¬ (φ ∨ ψ) ∧ x = B))) ↔ ((φ ∧ x = A) ∨ ((¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)))))
58		orass 218	. . . . 5 ⊢ (((φ ∨ ψ) ∨ (¬ (φ ∨ ψ) ∧ x = B)) ↔ (φ ∨ (ψ ∨ (¬ (φ ∨ ψ) ∧ x = B))))
59	57, 58, 22	3bitr4g 428	. . . 4 ⊢ (¬ (φ ∨ ψ) → (((φ ∨ ψ) ∨ (¬ (φ ∨ ψ) ∧ x = B)) ↔ ((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
60	59	bieudv 1013	. . 3 ⊢ (¬ (φ ∨ ψ) → (∃!x((φ ∨ ψ) ∨ (¬ (φ ∨ ψ) ∧ x = B)) ↔ ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))))
61	51, 60	mpbid 170	. 2 ⊢ (¬ (φ ∨ ψ) → ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C)))
62	25, 44, 61	ecase3 559	1 ⊢ ∃!x((φ ∧ x = A) ∨ (¬ (φ ∨ ψ) ∧ x = B) ∨ (ψ ∧ x = C))

Syntax hints:  ¬ wn 1   → wi 2   ∨ wo 195   ∧ wa 196   ∨ w3o 580  ∃!weu 1007   = wceq 1091   ∈ wcel 1092  Vcvv 1348

This theorem is referenced by:  moeq3 1432

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org