Theorem eueq3dc 2853

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
eueq3dc.1	⊢ 𝐴 ∈ V
eueq3dc.2	⊢ 𝐵 ∈ V
eueq3dc.3	⊢ 𝐶 ∈ V
eueq3dc.4	⊢ ¬ (𝜑 ∧ 𝜓)

Assertion

Ref	Expression
eueq3dc	⊢ (DECID 𝜑 → (DECID 𝜓 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))

Distinct variable groups:   𝜑,𝑥   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶

Proof of Theorem eueq3dc

Step	Hyp	Ref	Expression
1		dcor 919	. 2 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∨ 𝜓)))
2		df-dc 820	. . 3 ⊢ (DECID (𝜑 ∨ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
3		eueq3dc.1	. . . . . . 7 ⊢ 𝐴 ∈ V
4	3	eueq1 2851	. . . . . 6 ⊢ ∃!𝑥 𝑥 = 𝐴
5		ibar 299	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ (𝜑 ∧ 𝑥 = 𝐴)))
6		pm2.45 727	. . . . . . . . . . . . 13 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
7		eueq3dc.4	. . . . . . . . . . . . . . 15 ⊢ ¬ (𝜑 ∧ 𝜓)
8	7	imnani 680	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ 𝜓)
9	8	con2i 616	. . . . . . . . . . . . 13 ⊢ (𝜓 → ¬ 𝜑)
10	6, 9	jaoi 705	. . . . . . . . . . . 12 ⊢ ((¬ (𝜑 ∨ 𝜓) ∨ 𝜓) → ¬ 𝜑)
11	10	con2i 616	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (¬ (𝜑 ∨ 𝜓) ∨ 𝜓))
12	6	con2i 616	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ ¬ (𝜑 ∨ 𝜓))
13	12	bianfd 932	. . . . . . . . . . . 12 ⊢ (𝜑 → (¬ (𝜑 ∨ 𝜓) ↔ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
14	8	bianfd 932	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝑥 = 𝐶)))
15	13, 14	orbi12d 782	. . . . . . . . . . 11 ⊢ (𝜑 → ((¬ (𝜑 ∨ 𝜓) ∨ 𝜓) ↔ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
16	11, 15	mtbid 661	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
17		biorf 733	. . . . . . . . . 10 ⊢ (¬ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((𝜑 ∧ 𝑥 = 𝐴) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))))
18	16, 17	syl 14	. . . . . . . . 9 ⊢ (𝜑 → ((𝜑 ∧ 𝑥 = 𝐴) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))))
19	5, 18	bitrd 187	. . . . . . . 8 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴))))
20		3orrot 968	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (𝜑 ∧ 𝑥 = 𝐴)))
21		df-3or 963	. . . . . . . . 9 ⊢ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (𝜑 ∧ 𝑥 = 𝐴)) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴)))
22	20, 21	bitri 183	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (𝜑 ∧ 𝑥 = 𝐴)))
23	19, 22	syl6bbr 197	. . . . . . 7 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
24	23	eubidv 2005	. . . . . 6 ⊢ (𝜑 → (∃!𝑥 𝑥 = 𝐴 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
25	4, 24	mpbii 147	. . . . 5 ⊢ (𝜑 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
26		eueq3dc.3	. . . . . . 7 ⊢ 𝐶 ∈ V
27	26	eueq1 2851	. . . . . 6 ⊢ ∃!𝑥 𝑥 = 𝐶
28		ibar 299	. . . . . . . . 9 ⊢ (𝜓 → (𝑥 = 𝐶 ↔ (𝜓 ∧ 𝑥 = 𝐶)))
29	8	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ¬ 𝜓)
30		pm2.46 728	. . . . . . . . . . . . 13 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
31	30	adantr 274	. . . . . . . . . . . 12 ⊢ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) → ¬ 𝜓)
32	29, 31	jaoi 705	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) → ¬ 𝜓)
33	32	con2i 616	. . . . . . . . . 10 ⊢ (𝜓 → ¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
34		biorf 733	. . . . . . . . . 10 ⊢ (¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) → ((𝜓 ∧ 𝑥 = 𝐶) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
35	33, 34	syl 14	. . . . . . . . 9 ⊢ (𝜓 → ((𝜓 ∧ 𝑥 = 𝐶) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
36	28, 35	bitrd 187	. . . . . . . 8 ⊢ (𝜓 → (𝑥 = 𝐶 ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
37		df-3or 963	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
38	36, 37	syl6bbr 197	. . . . . . 7 ⊢ (𝜓 → (𝑥 = 𝐶 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
39	38	eubidv 2005	. . . . . 6 ⊢ (𝜓 → (∃!𝑥 𝑥 = 𝐶 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
40	27, 39	mpbii 147	. . . . 5 ⊢ (𝜓 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
41	25, 40	jaoi 705	. . . 4 ⊢ ((𝜑 ∨ 𝜓) → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
42		eueq3dc.2	. . . . . 6 ⊢ 𝐵 ∈ V
43	42	eueq1 2851	. . . . 5 ⊢ ∃!𝑥 𝑥 = 𝐵
44		ibar 299	. . . . . . . 8 ⊢ (¬ (𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
45		simpl 108	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜑)
46		simpl 108	. . . . . . . . . . 11 ⊢ ((𝜓 ∧ 𝑥 = 𝐶) → 𝜓)
47	45, 46	orim12i 748	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → (𝜑 ∨ 𝜓))
48	47	con3i 621	. . . . . . . . 9 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
49		biorf 733	. . . . . . . . 9 ⊢ (¬ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))))
50	48, 49	syl 14	. . . . . . . 8 ⊢ (¬ (𝜑 ∨ 𝜓) → ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))))
51	44, 50	bitrd 187	. . . . . . 7 ⊢ (¬ (𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))))
52		3orcomb 971	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
53		df-3or 963	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
54	52, 53	bitri 183	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵)))
55	51, 54	syl6bbr 197	. . . . . 6 ⊢ (¬ (𝜑 ∨ 𝜓) → (𝑥 = 𝐵 ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
56	55	eubidv 2005	. . . . 5 ⊢ (¬ (𝜑 ∨ 𝜓) → (∃!𝑥 𝑥 = 𝐵 ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))
57	43, 56	mpbii 147	. . . 4 ⊢ (¬ (𝜑 ∨ 𝜓) → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
58	41, 57	jaoi 705	. . 3 ⊢ (((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)) → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
59	2, 58	sylbi 120	. 2 ⊢ (DECID (𝜑 ∨ 𝜓) → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))
60	1, 59	syl6 33	1 ⊢ (DECID 𝜑 → (DECID 𝜓 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697  DECID wdc 819   ∨ w3o 961   = wceq 1331   ∈ wcel 1480  ∃!weu 1997  Vcvv 2681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-v 2683

This theorem is referenced by:  moeq3dc  2855