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 )