Metamath Proof Explorer

Theorem reuind

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

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

Proof

Step Hyp Ref Expression
1 reuind.1 
 |-  ( x = y -> ( ph <-> ps ) )
2 reuind.2 
 |-  ( x = y -> A = B )
3 2 eleq1d 
 |-  ( x = y -> ( A e. C <-> B e. C ) )
4 3 1 anbi12d 
 |-  ( x = y -> ( ( A e. C /\ ph ) <-> ( B e. C /\ ps ) ) )
5 4 cbvexvw 
 |-  ( E. x ( A e. C /\ ph ) <-> E. y ( B e. C /\ ps ) )
6 r19.41v 
 |-  ( E. z e. C ( z = B /\ ps ) <-> ( E. z e. C z = B /\ ps ) )
7 6 exbii 
 |-  ( E. y E. z e. C ( z = B /\ ps ) <-> E. y ( E. z e. C z = B /\ ps ) )
8 rexcom4 
 |-  ( E. z e. C E. y ( z = B /\ ps ) <-> E. y E. z e. C ( z = B /\ ps ) )
9 risset 
 |-  ( B e. C <-> E. z e. C z = B )
10 9 anbi1i 
 |-  ( ( B e. C /\ ps ) <-> ( E. z e. C z = B /\ ps ) )
11 10 exbii 
 |-  ( E. y ( B e. C /\ ps ) <-> E. y ( E. z e. C z = B /\ ps ) )
12 7 8 11 3bitr4ri 
 |-  ( E. y ( B e. C /\ ps ) <-> E. z e. C E. y ( z = B /\ ps ) )
13 5 12 bitri 
 |-  ( E. x ( A e. C /\ ph ) <-> E. z e. C E. y ( z = B /\ ps ) )
14 eqeq2 
 |-  ( A = B -> ( z = A <-> z = B ) )
15 14 imim2i 
 |-  ( ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> A = B ) -> ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> ( z = A <-> z = B ) ) )
16 biimpr 
 |-  ( ( z = A <-> z = B ) -> ( z = B -> z = A ) )
17 16 imim2i 
 |-  ( ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> ( z = A <-> z = B ) ) -> ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> ( z = B -> z = A ) ) )
18 an31 
 |-  ( ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) /\ z = B ) <-> ( ( z = B /\ ( B e. C /\ ps ) ) /\ ( A e. C /\ ph ) ) )
19 18 imbi1i 
 |-  ( ( ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) /\ z = B ) -> z = A ) <-> ( ( ( z = B /\ ( B e. C /\ ps ) ) /\ ( A e. C /\ ph ) ) -> z = A ) )
20 impexp 
 |-  ( ( ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) /\ z = B ) -> z = A ) <-> ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> ( z = B -> z = A ) ) )
21 impexp 
 |-  ( ( ( ( z = B /\ ( B e. C /\ ps ) ) /\ ( A e. C /\ ph ) ) -> z = A ) <-> ( ( z = B /\ ( B e. C /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) )
22 19 20 21 3bitr3i 
 |-  ( ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> ( z = B -> z = A ) ) <-> ( ( z = B /\ ( B e. C /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) )
23 17 22 sylib 
 |-  ( ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> ( z = A <-> z = B ) ) -> ( ( z = B /\ ( B e. C /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) )
24 15 23 syl 
 |-  ( ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> A = B ) -> ( ( z = B /\ ( B e. C /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) )
25 24 2alimi 
 |-  ( A. x A. y ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> A = B ) -> A. x A. y ( ( z = B /\ ( B e. C /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) )
26 19.23v 
 |-  ( A. y ( ( z = B /\ ( B e. C /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) <-> ( E. y ( z = B /\ ( B e. C /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) )
27 an12 
 |-  ( ( z = B /\ ( B e. C /\ ps ) ) <-> ( B e. C /\ ( z = B /\ ps ) ) )
28 eleq1 
 |-  ( z = B -> ( z e. C <-> B e. C ) )
29 28 adantr 
 |-  ( ( z = B /\ ps ) -> ( z e. C <-> B e. C ) )
30 29 pm5.32ri 
 |-  ( ( z e. C /\ ( z = B /\ ps ) ) <-> ( B e. C /\ ( z = B /\ ps ) ) )
31 27 30 bitr4i 
 |-  ( ( z = B /\ ( B e. C /\ ps ) ) <-> ( z e. C /\ ( z = B /\ ps ) ) )
32 31 exbii 
 |-  ( E. y ( z = B /\ ( B e. C /\ ps ) ) <-> E. y ( z e. C /\ ( z = B /\ ps ) ) )
33 19.42v 
 |-  ( E. y ( z e. C /\ ( z = B /\ ps ) ) <-> ( z e. C /\ E. y ( z = B /\ ps ) ) )
34 32 33 bitri 
 |-  ( E. y ( z = B /\ ( B e. C /\ ps ) ) <-> ( z e. C /\ E. y ( z = B /\ ps ) ) )
35 34 imbi1i 
 |-  ( ( E. y ( z = B /\ ( B e. C /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) <-> ( ( z e. C /\ E. y ( z = B /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) )
36 26 35 bitri 
 |-  ( A. y ( ( z = B /\ ( B e. C /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) <-> ( ( z e. C /\ E. y ( z = B /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) )
37 36 albii 
 |-  ( A. x A. y ( ( z = B /\ ( B e. C /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) <-> A. x ( ( z e. C /\ E. y ( z = B /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) )
38 19.21v 
 |-  ( A. x ( ( z e. C /\ E. y ( z = B /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) <-> ( ( z e. C /\ E. y ( z = B /\ ps ) ) -> A. x ( ( A e. C /\ ph ) -> z = A ) ) )
39 37 38 bitri 
 |-  ( A. x A. y ( ( z = B /\ ( B e. C /\ ps ) ) -> ( ( A e. C /\ ph ) -> z = A ) ) <-> ( ( z e. C /\ E. y ( z = B /\ ps ) ) -> A. x ( ( A e. C /\ ph ) -> z = A ) ) )
40 25 39 sylib 
 |-  ( A. x A. y ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> A = B ) -> ( ( z e. C /\ E. y ( z = B /\ ps ) ) -> A. x ( ( A e. C /\ ph ) -> z = A ) ) )
41 40 expd 
 |-  ( A. x A. y ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> A = B ) -> ( z e. C -> ( E. y ( z = B /\ ps ) -> A. x ( ( A e. C /\ ph ) -> z = A ) ) ) )
42 41 reximdvai 
 |-  ( A. x A. y ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> A = B ) -> ( E. z e. C E. y ( z = B /\ ps ) -> E. z e. C A. x ( ( A e. C /\ ph ) -> z = A ) ) )
43 13 42 syl5bi 
 |-  ( A. x A. y ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> A = B ) -> ( E. x ( A e. C /\ ph ) -> E. z e. C A. x ( ( A e. C /\ ph ) -> z = A ) ) )
44 43 imp 
 |-  ( ( A. x A. y ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> A = B ) /\ E. x ( A e. C /\ ph ) ) -> E. z e. C A. x ( ( A e. C /\ ph ) -> z = A ) )
45 pm4.24 
 |-  ( ( A e. C /\ ph ) <-> ( ( A e. C /\ ph ) /\ ( A e. C /\ ph ) ) )
46 45 biimpi 
 |-  ( ( A e. C /\ ph ) -> ( ( A e. C /\ ph ) /\ ( A e. C /\ ph ) ) )
47 anim12 
 |-  ( ( ( ( A e. C /\ ph ) -> z = A ) /\ ( ( A e. C /\ ph ) -> w = A ) ) -> ( ( ( A e. C /\ ph ) /\ ( A e. C /\ ph ) ) -> ( z = A /\ w = A ) ) )
48 eqtr3 
 |-  ( ( z = A /\ w = A ) -> z = w )
49 46 47 48 syl56 
 |-  ( ( ( ( A e. C /\ ph ) -> z = A ) /\ ( ( A e. C /\ ph ) -> w = A ) ) -> ( ( A e. C /\ ph ) -> z = w ) )
50 49 alanimi 
 |-  ( ( A. x ( ( A e. C /\ ph ) -> z = A ) /\ A. x ( ( A e. C /\ ph ) -> w = A ) ) -> A. x ( ( A e. C /\ ph ) -> z = w ) )
51 19.23v 
 |-  ( A. x ( ( A e. C /\ ph ) -> z = w ) <-> ( E. x ( A e. C /\ ph ) -> z = w ) )
52 50 51 sylib 
 |-  ( ( A. x ( ( A e. C /\ ph ) -> z = A ) /\ A. x ( ( A e. C /\ ph ) -> w = A ) ) -> ( E. x ( A e. C /\ ph ) -> z = w ) )
53 52 com12 
 |-  ( E. x ( A e. C /\ ph ) -> ( ( A. x ( ( A e. C /\ ph ) -> z = A ) /\ A. x ( ( A e. C /\ ph ) -> w = A ) ) -> z = w ) )
54 53 a1d 
 |-  ( E. x ( A e. C /\ ph ) -> ( ( z e. C /\ w e. C ) -> ( ( A. x ( ( A e. C /\ ph ) -> z = A ) /\ A. x ( ( A e. C /\ ph ) -> w = A ) ) -> z = w ) ) )
55 54 ralrimivv 
 |-  ( E. x ( A e. C /\ ph ) -> A. z e. C A. w e. C ( ( A. x ( ( A e. C /\ ph ) -> z = A ) /\ A. x ( ( A e. C /\ ph ) -> w = A ) ) -> z = w ) )
56 55 adantl 
 |-  ( ( A. x A. y ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> A = B ) /\ E. x ( A e. C /\ ph ) ) -> A. z e. C A. w e. C ( ( A. x ( ( A e. C /\ ph ) -> z = A ) /\ A. x ( ( A e. C /\ ph ) -> w = A ) ) -> z = w ) )
57 eqeq1 
 |-  ( z = w -> ( z = A <-> w = A ) )
58 57 imbi2d 
 |-  ( z = w -> ( ( ( A e. C /\ ph ) -> z = A ) <-> ( ( A e. C /\ ph ) -> w = A ) ) )
59 58 albidv 
 |-  ( z = w -> ( A. x ( ( A e. C /\ ph ) -> z = A ) <-> A. x ( ( A e. C /\ ph ) -> w = A ) ) )
60 59 reu4 
 |-  ( E! z e. C A. x ( ( A e. C /\ ph ) -> z = A ) <-> ( E. z e. C A. x ( ( A e. C /\ ph ) -> z = A ) /\ A. z e. C A. w e. C ( ( A. x ( ( A e. C /\ ph ) -> z = A ) /\ A. x ( ( A e. C /\ ph ) -> w = A ) ) -> z = w ) ) )
61 44 56 60 sylanbrc 
 |-  ( ( A. x A. y ( ( ( A e. C /\ ph ) /\ ( B e. C /\ ps ) ) -> A = B ) /\ E. x ( A e. C /\ ph ) ) -> E! z e. C A. x ( ( A e. C /\ ph ) -> z = A ) )