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 \in V$
	eueq3.2	$⊢ B \in V$
	eueq3.3	$⊢ C \in V$
	eueq3.4	$⊢ \neg (φ \land ψ)$
Assertion	eueq3	$⊢ \exists! x ((φ \land x = A) \lor (\neg (φ \lor ψ) \land x = B) \lor (ψ \land x = C))$

Proof

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

Metamath Proof Explorer

Theorem eueq3

Proof