Metamath Proof Explorer

Theorem lmmo

Description: A sequence in a Hausdorff space converges to at most one limit. Part of Lemma 1.4-2(a) of Kreyszig p. 26. (Contributed by NM, 31-Jan-2008) (Proof shortened by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmmo.1 
|- ( ph -> J e. Haus )
lmmo.4 
|- ( ph -> F ( ~~>t ` J ) A )
lmmo.5 
|- ( ph -> F ( ~~>t ` J ) B )
Assertion lmmo 
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 lmmo.1 
 |-  ( ph -> J e. Haus )
2 lmmo.4 
 |-  ( ph -> F ( ~~>t ` J ) A )
3 lmmo.5 
 |-  ( ph -> F ( ~~>t ` J ) B )
4 an4 
 |-  ( ( ( x e. J /\ y e. J ) /\ ( A e. x /\ B e. y ) ) <-> ( ( x e. J /\ A e. x ) /\ ( y e. J /\ B e. y ) ) )
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 simprr 
 |-  ( ( ph /\ ( x e. J /\ A e. x ) ) -> A e. x )
7 1zzd 
 |-  ( ( ph /\ ( x e. J /\ A e. x ) ) -> 1 e. ZZ )
8 2 adantr 
 |-  ( ( ph /\ ( x e. J /\ A e. x ) ) -> F ( ~~>t ` J ) A )
9 simprl 
 |-  ( ( ph /\ ( x e. J /\ A e. x ) ) -> x e. J )
10 5 6 7 8 9 lmcvg 
 |-  ( ( ph /\ ( x e. J /\ A e. x ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. x )
11 10 ex 
 |-  ( ph -> ( ( x e. J /\ A e. x ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. x ) )
12 simprr 
 |-  ( ( ph /\ ( y e. J /\ B e. y ) ) -> B e. y )
13 1zzd 
 |-  ( ( ph /\ ( y e. J /\ B e. y ) ) -> 1 e. ZZ )
14 3 adantr 
 |-  ( ( ph /\ ( y e. J /\ B e. y ) ) -> F ( ~~>t ` J ) B )
15 simprl 
 |-  ( ( ph /\ ( y e. J /\ B e. y ) ) -> y e. J )
16 5 12 13 14 15 lmcvg 
 |-  ( ( ph /\ ( y e. J /\ B e. y ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. y )
17 16 ex 
 |-  ( ph -> ( ( y e. J /\ B e. y ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. y ) )
18 11 17 anim12d 
 |-  ( ph -> ( ( ( x e. J /\ A e. x ) /\ ( y e. J /\ B e. y ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. x /\ E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. y ) ) )
19 5 rexanuz2 
 |-  ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) <-> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. x /\ E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. y ) )
20 nnz 
 |-  ( j e. NN -> j e. ZZ )
21 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
22 ne0i 
 |-  ( j e. ( ZZ>= ` j ) -> ( ZZ>= ` j ) =/= (/) )
23 20 21 22 3syl 
 |-  ( j e. NN -> ( ZZ>= ` j ) =/= (/) )
24 r19.2z 
 |-  ( ( ( ZZ>= ` j ) =/= (/) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) ) -> E. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) )
25 elin 
 |-  ( ( F ` k ) e. ( x i^i y ) <-> ( ( F ` k ) e. x /\ ( F ` k ) e. y ) )
26 n0i 
 |-  ( ( F ` k ) e. ( x i^i y ) -> -. ( x i^i y ) = (/) )
27 25 26 sylbir 
 |-  ( ( ( F ` k ) e. x /\ ( F ` k ) e. y ) -> -. ( x i^i y ) = (/) )
28 27 rexlimivw 
 |-  ( E. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) -> -. ( x i^i y ) = (/) )
29 24 28 syl 
 |-  ( ( ( ZZ>= ` j ) =/= (/) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) ) -> -. ( x i^i y ) = (/) )
30 23 29 sylan 
 |-  ( ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) ) -> -. ( x i^i y ) = (/) )
31 30 rexlimiva 
 |-  ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) -> -. ( x i^i y ) = (/) )
32 19 31 sylbir 
 |-  ( ( E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. x /\ E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. y ) -> -. ( x i^i y ) = (/) )
33 18 32 syl6 
 |-  ( ph -> ( ( ( x e. J /\ A e. x ) /\ ( y e. J /\ B e. y ) ) -> -. ( x i^i y ) = (/) ) )
34 4 33 syl5bi 
 |-  ( ph -> ( ( ( x e. J /\ y e. J ) /\ ( A e. x /\ B e. y ) ) -> -. ( x i^i y ) = (/) ) )
35 34 expdimp 
 |-  ( ( ph /\ ( x e. J /\ y e. J ) ) -> ( ( A e. x /\ B e. y ) -> -. ( x i^i y ) = (/) ) )
36 imnan 
 |-  ( ( ( A e. x /\ B e. y ) -> -. ( x i^i y ) = (/) ) <-> -. ( ( A e. x /\ B e. y ) /\ ( x i^i y ) = (/) ) )
37 35 36 sylib 
 |-  ( ( ph /\ ( x e. J /\ y e. J ) ) -> -. ( ( A e. x /\ B e. y ) /\ ( x i^i y ) = (/) ) )
38 df-3an 
 |-  ( ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) <-> ( ( A e. x /\ B e. y ) /\ ( x i^i y ) = (/) ) )
39 37 38 sylnibr 
 |-  ( ( ph /\ ( x e. J /\ y e. J ) ) -> -. ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) )
40 39 anassrs 
 |-  ( ( ( ph /\ x e. J ) /\ y e. J ) -> -. ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) )
41 40 nrexdv 
 |-  ( ( ph /\ x e. J ) -> -. E. y e. J ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) )
42 41 nrexdv 
 |-  ( ph -> -. E. x e. J E. y e. J ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) )
43 haustop 
 |-  ( J e. Haus -> J e. Top )
44 1 43 syl 
 |-  ( ph -> J e. Top )
45 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
46 44 45 sylib 
 |-  ( ph -> J e. ( TopOn ` U. J ) )
47 lmcl 
 |-  ( ( J e. ( TopOn ` U. J ) /\ F ( ~~>t ` J ) A ) -> A e. U. J )
48 46 2 47 syl2anc 
 |-  ( ph -> A e. U. J )
49 lmcl 
 |-  ( ( J e. ( TopOn ` U. J ) /\ F ( ~~>t ` J ) B ) -> B e. U. J )
50 46 3 49 syl2anc 
 |-  ( ph -> B e. U. J )
51 eqid 
 |-  U. J = U. J
52 51 hausnei 
 |-  ( ( J e. Haus /\ ( A e. U. J /\ B e. U. J /\ A =/= B ) ) -> E. x e. J E. y e. J ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) )
53 52 3exp2 
 |-  ( J e. Haus -> ( A e. U. J -> ( B e. U. J -> ( A =/= B -> E. x e. J E. y e. J ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) ) ) ) )
54 1 48 50 53 syl3c 
 |-  ( ph -> ( A =/= B -> E. x e. J E. y e. J ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) ) )
55 54 necon1bd 
 |-  ( ph -> ( -. E. x e. J E. y e. J ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) -> A = B ) )
56 42 55 mpd 
 |-  ( ph -> A = B )