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 ) )