Theorem eueq3 1919

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

Hypotheses

Ref	Expression
eueq3.1	|- A e. V
eueq3.2	|- B e. V
eueq3.3	|- C e. V
eueq3.4	|- -. (ph /\ ps)

Assertion

Ref	Expression
eueq3	|- E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))

Distinct variable groups:   ph,x   ps,x   x,A   x,B   x,C

Proof of Theorem eueq3

Step	Hyp	Ref	Expression
1		euorv 1399	. . . 4 |- ((-. (-. (ph \/ ps) \/ ps) /\ E!x(ph /\ x = A)) -> E!x((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)))
2		pm2.45 277	. . . . . 6 |- (-. (ph \/ ps) -> -. ph)
3		eueq3.4	. . . . . . . 8 |- -. (ph /\ ps)
4		imnan 242	. . . . . . . 8 |- ((ph -> -. ps) <-> -. (ph /\ ps))
5	3, 4	mpbir 190	. . . . . . 7 |- (ph -> -. ps)
6	5	con2i 97	. . . . . 6 |- (ps -> -. ph)
7	2, 6	jaoi 341	. . . . 5 |- ((-. (ph \/ ps) \/ ps) -> -. ph)
8	7	con2i 97	. . . 4 |- (ph -> -. (-. (ph \/ ps) \/ ps))
9		eueq3.1	. . . . . 6 |- A e. V
10	9	eueq1 1917	. . . . 5 |- E!x x = A
11		euanv 1432	. . . . . 6 |- (E!x(ph /\ x = A) <-> (ph /\ E!x x = A))
12	11	biimpr 152	. . . . 5 |- ((ph /\ E!x x = A) -> E!x(ph /\ x = A))
13	10, 12	mpan2 696	. . . 4 |- (ph -> E!x(ph /\ x = A))
14	1, 8, 13	sylanc 471	. . 3 |- (ph -> E!x((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)))
15		negb 86	. . . . . . . . 9 |- ((ph \/ ps) -> -. -. (ph \/ ps))
16	15	orcs 274	. . . . . . . 8 |- (ph -> -. -. (ph \/ ps))
17	16	bianfd 738	. . . . . . 7 |- (ph -> (-. (ph \/ ps) <-> (-. (ph \/ ps) /\ x = B)))
18	5	bianfd 738	. . . . . . 7 |- (ph -> (ps <-> (ps /\ x = C)))
19	17, 18	orbi12d 627	. . . . . 6 |- (ph -> ((-. (ph \/ ps) \/ ps) <-> ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
20	19	orbi2d 614	. . . . 5 |- (ph -> (((ph /\ x = A) \/ (-. (ph \/ ps) \/ ps)) <-> ((ph /\ x = A) \/ ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))))
21		orcom 246	. . . . 5 |- (((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) \/ ps)))
22		3orass 778	. . . . 5 |- (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) <-> ((ph /\ x = A) \/ ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
23	20, 21, 22	3bitr4g 555	. . . 4 |- (ph -> (((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
24	23	eubidv 1386	. . 3 |- (ph -> (E!x((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)) <-> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
25	14, 24	mpbid 195	. 2 |- (ph -> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
26		euorv 1399	. . . 4 |- ((-. (ph \/ -. (ph \/ ps)) /\ E!x(ps /\ x = C)) -> E!x((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)))
27		pm2.46 278	. . . . . 6 |- (-. (ph \/ ps) -> -. ps)
28	5, 27	jaoi 341	. . . . 5 |- ((ph \/ -. (ph \/ ps)) -> -. ps)
29	28	con2i 97	. . . 4 |- (ps -> -. (ph \/ -. (ph \/ ps)))
30		eueq3.3	. . . . . 6 |- C e. V
31	30	eueq1 1917	. . . . 5 |- E!x x = C
32		euanv 1432	. . . . . 6 |- (E!x(ps /\ x = C) <-> (ps /\ E!x x = C))
33	32	biimpr 152	. . . . 5 |- ((ps /\ E!x x = C) -> E!x(ps /\ x = C))
34	31, 33	mpan2 696	. . . 4 |- (ps -> E!x(ps /\ x = C))
35	26, 29, 34	sylanc 471	. . 3 |- (ps -> E!x((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)))
36	6	bianfd 738	. . . . . . 7 |- (ps -> (ph <-> (ph /\ x = A)))
37	15	olcs 275	. . . . . . . 8 |- (ps -> -. -. (ph \/ ps))
38	37	bianfd 738	. . . . . . 7 |- (ps -> (-. (ph \/ ps) <-> (-. (ph \/ ps) /\ x = B)))
39	36, 38	orbi12d 627	. . . . . 6 |- (ps -> ((ph \/ -. (ph \/ ps)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B))))
40	39	orbi1d 615	. . . . 5 |- (ps -> (((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)) <-> (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B)) \/ (ps /\ x = C))))
41		df-3or 776	. . . . 5 |- (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)) <-> (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B)) \/ (ps /\ x = C)))
42	40, 41	syl6bbr 538	. . . 4 |- (ps -> (((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
43	42	eubidv 1386	. . 3 |- (ps -> (E!x((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)) <-> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
44	35, 43	mpbid 195	. 2 |- (ps -> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
45		eueq3.2	. . . . . 6 |- B e. V
46	45	eueq1 1917	. . . . 5 |- E!x x = B
47		euanv 1432	. . . . . 6 |- (E!x(-. (ph \/ ps) /\ x = B) <-> (-. (ph \/ ps) /\ E!x x = B))
48	47	biimpr 152	. . . . 5 |- ((-. (ph \/ ps) /\ E!x x = B) -> E!x(-. (ph \/ ps) /\ x = B))
49	46, 48	mpan2 696	. . . 4 |- (-. (ph \/ ps) -> E!x(-. (ph \/ ps) /\ x = B))
50		euorv 1399	. . . 4 |- ((-. (ph \/ ps) /\ E!x(-. (ph \/ ps) /\ x = B)) -> E!x((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)))
51	49, 50	mpdan 704	. . 3 |- (-. (ph \/ ps) -> E!x((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)))
52	2	bianfd 738	. . . . . 6 |- (-. (ph \/ ps) -> (ph <-> (ph /\ x = A)))
53	27	bianfd 738	. . . . . . . 8 |- (-. (ph \/ ps) -> (ps <-> (ps /\ x = C)))
54	53	orbi1d 615	. . . . . . 7 |- (-. (ph \/ ps) -> ((ps \/ (-. (ph \/ ps) /\ x = B)) <-> ((ps /\ x = C) \/ (-. (ph \/ ps) /\ x = B))))
55		orcom 246	. . . . . . 7 |- (((ps /\ x = C) \/ (-. (ph \/ ps) /\ x = B)) <-> ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
56	54, 55	syl6bb 536	. . . . . 6 |- (-. (ph \/ ps) -> ((ps \/ (-. (ph \/ ps) /\ x = B)) <-> ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
57	52, 56	orbi12d 627	. . . . 5 |- (-. (ph \/ ps) -> ((ph \/ (ps \/ (-. (ph \/ ps) /\ x = B))) <-> ((ph /\ x = A) \/ ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))))
58		orass 260	. . . . 5 |- (((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)) <-> (ph \/ (ps \/ (-. (ph \/ ps) /\ x = B))))
59	57, 58, 22	3bitr4g 555	. . . 4 |- (-. (ph \/ ps) -> (((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
60	59	eubidv 1386	. . 3 |- (-. (ph \/ ps) -> (E!x((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)) <-> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
61	51, 60	mpbid 195	. 2 |- (-. (ph \/ ps) -> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
62	25, 44, 61	ecase3 752	1 |- E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 222   /\ wa 223   \/ w3o 774   = wceq</