Metamath Proof Explorer

Theorem euind

Description: Existential uniqueness via an indirect equality. (Contributed by NM, 11-Oct-2010)

Ref Expression
Hypotheses euind.1 
|- B e. _V
euind.2 
|- ( x = y -> ( ph <-> ps ) )
Assertion euind 
|- ( ( A. x A. y ( ( ph /\ ps ) -> A = B ) /\ E. x ph ) -> E! z A. x ( ph -> z = A ) )

Proof

Step Hyp Ref Expression
1 euind.1 
 |-  B e. _V
2 euind.2 
 |-  ( x = y -> ( ph <-> ps ) )
3 2 cbvexvw 
 |-  ( E. x ph <-> E. y ps )
4 1 isseti 
 |-  E. z z = B
5 4 biantrur 
 |-  ( ps <-> ( E. z z = B /\ ps ) )
6 5 exbii 
 |-  ( E. y ps <-> E. y ( E. z z = B /\ ps ) )
7 19.41v 
 |-  ( E. z ( z = B /\ ps ) <-> ( E. z z = B /\ ps ) )
8 7 exbii 
 |-  ( E. y E. z ( z = B /\ ps ) <-> E. y ( E. z z = B /\ ps ) )
9 excom 
 |-  ( E. y E. z ( z = B /\ ps ) <-> E. z E. y ( z = B /\ ps ) )
10 6 8 9 3bitr2i 
 |-  ( E. y ps <-> E. z E. y ( z = B /\ ps ) )
11 3 10 bitri 
 |-  ( E. x ph <-> E. z E. y ( z = B /\ ps ) )
12 eqeq2 
 |-  ( A = B -> ( z = A <-> z = B ) )
13 12 imim2i 
 |-  ( ( ( ph /\ ps ) -> A = B ) -> ( ( ph /\ ps ) -> ( z = A <-> z = B ) ) )
14 biimpr 
 |-  ( ( z = A <-> z = B ) -> ( z = B -> z = A ) )
15 14 imim2i 
 |-  ( ( ( ph /\ ps ) -> ( z = A <-> z = B ) ) -> ( ( ph /\ ps ) -> ( z = B -> z = A ) ) )
16 an31 
 |-  ( ( ( ph /\ ps ) /\ z = B ) <-> ( ( z = B /\ ps ) /\ ph ) )
17 16 imbi1i 
 |-  ( ( ( ( ph /\ ps ) /\ z = B ) -> z = A ) <-> ( ( ( z = B /\ ps ) /\ ph ) -> z = A ) )
18 impexp 
 |-  ( ( ( ( ph /\ ps ) /\ z = B ) -> z = A ) <-> ( ( ph /\ ps ) -> ( z = B -> z = A ) ) )
19 impexp 
 |-  ( ( ( ( z = B /\ ps ) /\ ph ) -> z = A ) <-> ( ( z = B /\ ps ) -> ( ph -> z = A ) ) )
20 17 18 19 3bitr3i 
 |-  ( ( ( ph /\ ps ) -> ( z = B -> z = A ) ) <-> ( ( z = B /\ ps ) -> ( ph -> z = A ) ) )
21 15 20 sylib 
 |-  ( ( ( ph /\ ps ) -> ( z = A <-> z = B ) ) -> ( ( z = B /\ ps ) -> ( ph -> z = A ) ) )
22 13 21 syl 
 |-  ( ( ( ph /\ ps ) -> A = B ) -> ( ( z = B /\ ps ) -> ( ph -> z = A ) ) )
23 22 2alimi 
 |-  ( A. x A. y ( ( ph /\ ps ) -> A = B ) -> A. x A. y ( ( z = B /\ ps ) -> ( ph -> z = A ) ) )
24 19.23v 
 |-  ( A. y ( ( z = B /\ ps ) -> ( ph -> z = A ) ) <-> ( E. y ( z = B /\ ps ) -> ( ph -> z = A ) ) )
25 24 albii 
 |-  ( A. x A. y ( ( z = B /\ ps ) -> ( ph -> z = A ) ) <-> A. x ( E. y ( z = B /\ ps ) -> ( ph -> z = A ) ) )
26 19.21v 
 |-  ( A. x ( E. y ( z = B /\ ps ) -> ( ph -> z = A ) ) <-> ( E. y ( z = B /\ ps ) -> A. x ( ph -> z = A ) ) )
27 25 26 bitri 
 |-  ( A. x A. y ( ( z = B /\ ps ) -> ( ph -> z = A ) ) <-> ( E. y ( z = B /\ ps ) -> A. x ( ph -> z = A ) ) )
28 23 27 sylib 
 |-  ( A. x A. y ( ( ph /\ ps ) -> A = B ) -> ( E. y ( z = B /\ ps ) -> A. x ( ph -> z = A ) ) )
29 28 eximdv 
 |-  ( A. x A. y ( ( ph /\ ps ) -> A = B ) -> ( E. z E. y ( z = B /\ ps ) -> E. z A. x ( ph -> z = A ) ) )
30 11 29 syl5bi 
 |-  ( A. x A. y ( ( ph /\ ps ) -> A = B ) -> ( E. x ph -> E. z A. x ( ph -> z = A ) ) )
31 30 imp 
 |-  ( ( A. x A. y ( ( ph /\ ps ) -> A = B ) /\ E. x ph ) -> E. z A. x ( ph -> z = A ) )
32 pm4.24 
 |-  ( ph <-> ( ph /\ ph ) )
33 32 biimpi 
 |-  ( ph -> ( ph /\ ph ) )
34 anim12 
 |-  ( ( ( ph -> z = A ) /\ ( ph -> w = A ) ) -> ( ( ph /\ ph ) -> ( z = A /\ w = A ) ) )
35 eqtr3 
 |-  ( ( z = A /\ w = A ) -> z = w )
36 33 34 35 syl56 
 |-  ( ( ( ph -> z = A ) /\ ( ph -> w = A ) ) -> ( ph -> z = w ) )
37 36 alanimi 
 |-  ( ( A. x ( ph -> z = A ) /\ A. x ( ph -> w = A ) ) -> A. x ( ph -> z = w ) )
38 19.23v 
 |-  ( A. x ( ph -> z = w ) <-> ( E. x ph -> z = w ) )
39 37 38 sylib 
 |-  ( ( A. x ( ph -> z = A ) /\ A. x ( ph -> w = A ) ) -> ( E. x ph -> z = w ) )
40 39 com12 
 |-  ( E. x ph -> ( ( A. x ( ph -> z = A ) /\ A. x ( ph -> w = A ) ) -> z = w ) )
41 40 alrimivv 
 |-  ( E. x ph -> A. z A. w ( ( A. x ( ph -> z = A ) /\ A. x ( ph -> w = A ) ) -> z = w ) )
42 41 adantl 
 |-  ( ( A. x A. y ( ( ph /\ ps ) -> A = B ) /\ E. x ph ) -> A. z A. w ( ( A. x ( ph -> z = A ) /\ A. x ( ph -> w = A ) ) -> z = w ) )
43 eqeq1 
 |-  ( z = w -> ( z = A <-> w = A ) )
44 43 imbi2d 
 |-  ( z = w -> ( ( ph -> z = A ) <-> ( ph -> w = A ) ) )
45 44 albidv 
 |-  ( z = w -> ( A. x ( ph -> z = A ) <-> A. x ( ph -> w = A ) ) )
46 45 eu4 
 |-  ( E! z A. x ( ph -> z = A ) <-> ( E. z A. x ( ph -> z = A ) /\ A. z A. w ( ( A. x ( ph -> z = A ) /\ A. x ( ph -> w = A ) ) -> z = w ) ) )
47 31 42 46 sylanbrc 
 |-  ( ( A. x A. y ( ( ph /\ ps ) -> A = B ) /\ E. x ph ) -> E! z A. x ( ph -> z = A ) )