Metamath Proof Explorer

Theorem 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 e. _V
eueq3.2 
|- B e. _V
eueq3.3 
|- C e. _V
eueq3.4 
|- -. ( ph /\ ps )
Assertion eueq3 
|- E! x ( ( ph /\ x = A ) \/ ( -. ( ph \/ ps ) /\ x = B ) \/ ( ps /\ x = C ) )

Proof

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