Theorem eueq3 2430

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		pm2.45 299	. . . . . 6 |- (-. (ph \/ ps) -> -. ph)
2		eueq3.4	. . . . . . . 8 |- -. (ph /\ ps)
3		imnan 261	. . . . . . . 8 |- ((ph -> -. ps) <-> -. (ph /\ ps))
4	2, 3	mpbir 207	. . . . . . 7 |- (ph -> -. ps)
5	4	con2i 113	. . . . . 6 |- (ps -> -. ph)
6	1, 5	jaoi 368	. . . . 5 |- ((-. (ph \/ ps) \/ ps) -> -. ph)
7	6	con2i 113	. . . 4 |- (ph -> -. (-. (ph \/ ps) \/ ps))
8		eueq3.1	. . . . . 6 |- A e. _V
9	8	eueq1 2428	. . . . 5 |- E!x x = A
10		euanv 1832	. . . . . 6 |- (E!x(ph /\ x = A) <-> (ph /\ E!x x = A))
11	10	biimpri 169	. . . . 5 |- ((ph /\ E!x x = A) -> E!x(ph /\ x = A))
12	9, 11	mpan2 760	. . . 4 |- (ph -> E!x(ph /\ x = A))
13		euorv 1794	. . . 4 |- ((-. (-. (ph \/ ps) \/ ps) /\ E!x(ph /\ x = A)) -> E!x((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)))
14	7, 12, 13	syl11anc 524	. . 3 |- (ph -> E!x((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)))
15		notnot1 102	. . . . . . . . 9 |- ((ph \/ ps) -> -. -. (ph \/ ps))
16	15	orcs 296	. . . . . . . 8 |- (ph -> -. -. (ph \/ ps))
17	16	bianfd 810	. . . . . . 7 |- (ph -> (-. (ph \/ ps) <-> (-. (ph \/ ps) /\ x = B)))
18	4	bianfd 810	. . . . . . 7 |- (ph -> (ps <-> (ps /\ x = C)))
19	17, 18	orbi12d 689	. . . . . 6 |- (ph -> ((-. (ph \/ ps) \/ ps) <-> ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
20	19	orbi2d 676	. . . . 5 |- (ph -> (((ph /\ x = A) \/ (-. (ph \/ ps) \/ ps)) <-> ((ph /\ x = A) \/ ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))))
21		orcom 266	. . . . 5 |- (((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) \/ ps)))
22		3orass 861	. . . . 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 614	. . . 4 |- (ph -> (((-. (ph \/ ps) \/ ps) \/ (ph /\ x = A)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
24	23	eubidv 1779	. . 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 212	. 2 |- (ph -> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
26		pm2.46 300	. . . . . 6 |- (-. (ph \/ ps) -> -. ps)
27	4, 26	jaoi 368	. . . . 5 |- ((ph \/ -. (ph \/ ps)) -> -. ps)
28	27	con2i 113	. . . 4 |- (ps -> -. (ph \/ -. (ph \/ ps)))
29		eueq3.3	. . . . . 6 |- C e. _V
30	29	eueq1 2428	. . . . 5 |- E!x x = C
31		euanv 1832	. . . . . 6 |- (E!x(ps /\ x = C) <-> (ps /\ E!x x = C))
32	31	biimpri 169	. . . . 5 |- ((ps /\ E!x x = C) -> E!x(ps /\ x = C))
33	30, 32	mpan2 760	. . . 4 |- (ps -> E!x(ps /\ x = C))
34		euorv 1794	. . . 4 |- ((-. (ph \/ -. (ph \/ ps)) /\ E!x(ps /\ x = C)) -> E!x((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)))
35	28, 33, 34	syl11anc 524	. . 3 |- (ps -> E!x((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)))
36	5	bianfd 810	. . . . . . 7 |- (ps -> (ph <-> (ph /\ x = A)))
37	15	olcs 297	. . . . . . . 8 |- (ps -> -. -. (ph \/ ps))
38	37	bianfd 810	. . . . . . 7 |- (ps -> (-. (ph \/ ps) <-> (-. (ph \/ ps) /\ x = B)))
39	36, 38	orbi12d 689	. . . . . 6 |- (ps -> ((ph \/ -. (ph \/ ps)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B))))
40	39	orbi1d 677	. . . . 5 |- (ps -> (((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)) <-> (((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B)) \/ (ps /\ x = C))))
41		df-3or 859	. . . . 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 597	. . . 4 |- (ps -> (((ph \/ -. (ph \/ ps)) \/ (ps /\ x = C)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
43	42	eubidv 1779	. . 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 212	. 2 |- (ps -> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
45		eueq3.2	. . . . . 6 |- B e. _V
46	45	eueq1 2428	. . . . 5 |- E!x x = B
47		euanv 1832	. . . . . 6 |- (E!x(-. (ph \/ ps) /\ x = B) <-> (-. (ph \/ ps) /\ E!x x = B))
48	47	biimpri 169	. . . . 5 |- ((-. (ph \/ ps) /\ E!x x = B) -> E!x(-. (ph \/ ps) /\ x = B))
49	46, 48	mpan2 760	. . . 4 |- (-. (ph \/ ps) -> E!x(-. (ph \/ ps) /\ x = B))
50		euorv 1794	. . . 4 |- ((-. (ph \/ ps) /\ E!x(-. (ph \/ ps) /\ x = B)) -> E!x((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)))
51	49, 50	mpdan 768	. . 3 |- (-. (ph \/ ps) -> E!x((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)))
52	1	bianfd 810	. . . . . 6 |- (-. (ph \/ ps) -> (ph <-> (ph /\ x = A)))
53	26	bianfd 810	. . . . . . . 8 |- (-. (ph \/ ps) -> (ps <-> (ps /\ x = C)))
54	53	orbi1d 677	. . . . . . 7 |- (-. (ph \/ ps) -> ((ps \/ (-. (ph \/ ps) /\ x = B)) <-> ((ps /\ x = C) \/ (-. (ph \/ ps) /\ x = B))))
55		orcom 266	. . . . . . 7 |- (((ps /\ x = C) \/ (-. (ph \/ ps) /\ x = B)) <-> ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
56	54, 55	syl6bb 595	. . . . . 6 |- (-. (ph \/ ps) -> ((ps \/ (-. (ph \/ ps) /\ x = B)) <-> ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
57	52, 56	orbi12d 689	. . . . 5 |- (-. (ph \/ ps) -> ((ph \/ (ps \/ (-. (ph \/ ps) /\ x = B))) <-> ((ph /\ x = A) \/ ((-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))))
58		orass 280	. . . . 5 |- (((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)) <-> (ph \/ (ps \/ (-. (ph \/ ps) /\ x = B))))
59	57, 58, 22	3bitr4g 614	. . . 4 |- (-. (ph \/ ps) -> (((ph \/ ps) \/ (-. (ph \/ ps) /\ x = B)) <-> ((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))))
60	59	eubidv 1779	. . 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 212	. 2 |- (-. (ph \/ ps) -> E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C)))
62	25, 44, 61	ecase3 825	1 |- E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 239   /\ wa 240   \/ w3o 857   = wceq 1298   e. wcel 1300  E!weu 1771  _Vcvv 2292

This theorem is referenced by:  moeq3 2432

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294

Copyright terms: Public domain