Metamath Proof Explorer


Theorem hausflimi

Description: One direction of hausflim . A filter in a Hausdorff space has at most one limit. (Contributed by FL, 14-Nov-2010) (Revised by Mario Carneiro, 21-Sep-2015)

Ref Expression
Assertion hausflimi
|- ( J e. Haus -> E* x x e. ( J fLim F ) )

Proof

Step Hyp Ref Expression
1 simpl
 |-  ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) -> J e. Haus )
2 simprll
 |-  ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) -> x e. ( J fLim F ) )
3 eqid
 |-  U. J = U. J
4 3 flimelbas
 |-  ( x e. ( J fLim F ) -> x e. U. J )
5 2 4 syl
 |-  ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) -> x e. U. J )
6 simprlr
 |-  ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) -> y e. ( J fLim F ) )
7 3 flimelbas
 |-  ( y e. ( J fLim F ) -> y e. U. J )
8 6 7 syl
 |-  ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) -> y e. U. J )
9 simprr
 |-  ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) -> x =/= y )
10 3 hausnei
 |-  ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) -> E. u e. J E. v e. J ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) )
11 1 5 8 9 10 syl13anc
 |-  ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) -> E. u e. J E. v e. J ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) )
12 df-3an
 |-  ( ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) <-> ( ( x e. u /\ y e. v ) /\ ( u i^i v ) = (/) ) )
13 simprl
 |-  ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) -> ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) )
14 hausflimlem
 |-  ( ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ ( u e. J /\ v e. J ) /\ ( x e. u /\ y e. v ) ) -> ( u i^i v ) =/= (/) )
15 14 3expa
 |-  ( ( ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ ( u e. J /\ v e. J ) ) /\ ( x e. u /\ y e. v ) ) -> ( u i^i v ) =/= (/) )
16 13 15 sylanl1
 |-  ( ( ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) /\ ( u e. J /\ v e. J ) ) /\ ( x e. u /\ y e. v ) ) -> ( u i^i v ) =/= (/) )
17 16 a1d
 |-  ( ( ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) /\ ( u e. J /\ v e. J ) ) /\ ( x e. u /\ y e. v ) ) -> ( x =/= y -> ( u i^i v ) =/= (/) ) )
18 17 necon4d
 |-  ( ( ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) /\ ( u e. J /\ v e. J ) ) /\ ( x e. u /\ y e. v ) ) -> ( ( u i^i v ) = (/) -> x = y ) )
19 18 expimpd
 |-  ( ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) /\ ( u e. J /\ v e. J ) ) -> ( ( ( x e. u /\ y e. v ) /\ ( u i^i v ) = (/) ) -> x = y ) )
20 12 19 syl5bi
 |-  ( ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) /\ ( u e. J /\ v e. J ) ) -> ( ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) -> x = y ) )
21 20 rexlimdvva
 |-  ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) -> ( E. u e. J E. v e. J ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) -> x = y ) )
22 11 21 mpd
 |-  ( ( J e. Haus /\ ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) /\ x =/= y ) ) -> x = y )
23 22 expr
 |-  ( ( J e. Haus /\ ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) ) -> ( x =/= y -> x = y ) )
24 23 necon1bd
 |-  ( ( J e. Haus /\ ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) ) -> ( -. x = y -> x = y ) )
25 24 pm2.18d
 |-  ( ( J e. Haus /\ ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) ) -> x = y )
26 25 ex
 |-  ( J e. Haus -> ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) -> x = y ) )
27 26 alrimivv
 |-  ( J e. Haus -> A. x A. y ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) -> x = y ) )
28 eleq1w
 |-  ( x = y -> ( x e. ( J fLim F ) <-> y e. ( J fLim F ) ) )
29 28 mo4
 |-  ( E* x x e. ( J fLim F ) <-> A. x A. y ( ( x e. ( J fLim F ) /\ y e. ( J fLim F ) ) -> x = y ) )
30 27 29 sylibr
 |-  ( J e. Haus -> E* x x e. ( J fLim F ) )