Metamath Proof Explorer

Theorem ufilcmp

Description: A space is compact iff every ultrafilter converges. (Contributed by Jeff Hankins, 11-Dec-2009) (Proof shortened by Mario Carneiro, 12-Apr-2015) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ufilcmp 
|- ( ( X e. UFL /\ J e. ( TopOn ` X ) ) -> ( J e. Comp <-> A. f e. ( UFil ` X ) ( J fLim f ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 ufilfil 
 |-  ( f e. ( UFil ` U. J ) -> f e. ( Fil ` U. J ) )
2 eqid 
 |-  U. J = U. J
3 2 fclscmpi 
 |-  ( ( J e. Comp /\ f e. ( Fil ` U. J ) ) -> ( J fClus f ) =/= (/) )
4 1 3 sylan2 
 |-  ( ( J e. Comp /\ f e. ( UFil ` U. J ) ) -> ( J fClus f ) =/= (/) )
5 4 ralrimiva 
 |-  ( J e. Comp -> A. f e. ( UFil ` U. J ) ( J fClus f ) =/= (/) )
6 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
7 6 fveq2d 
 |-  ( J e. ( TopOn ` X ) -> ( UFil ` X ) = ( UFil ` U. J ) )
8 7 raleqdv 
 |-  ( J e. ( TopOn ` X ) -> ( A. f e. ( UFil ` X ) ( J fClus f ) =/= (/) <-> A. f e. ( UFil ` U. J ) ( J fClus f ) =/= (/) ) )
9 8 adantl 
 |-  ( ( X e. UFL /\ J e. ( TopOn ` X ) ) -> ( A. f e. ( UFil ` X ) ( J fClus f ) =/= (/) <-> A. f e. ( UFil ` U. J ) ( J fClus f ) =/= (/) ) )
10 5 9 syl5ibr 
 |-  ( ( X e. UFL /\ J e. ( TopOn ` X ) ) -> ( J e. Comp -> A. f e. ( UFil ` X ) ( J fClus f ) =/= (/) ) )
11 ufli 
 |-  ( ( X e. UFL /\ g e. ( Fil ` X ) ) -> E. f e. ( UFil ` X ) g C_ f )
12 11 adantlr 
 |-  ( ( ( X e. UFL /\ J e. ( TopOn ` X ) ) /\ g e. ( Fil ` X ) ) -> E. f e. ( UFil ` X ) g C_ f )
13 r19.29 
 |-  ( ( A. f e. ( UFil ` X ) ( J fClus f ) =/= (/) /\ E. f e. ( UFil ` X ) g C_ f ) -> E. f e. ( UFil ` X ) ( ( J fClus f ) =/= (/) /\ g C_ f ) )
14 simpllr 
 |-  ( ( ( ( X e. UFL /\ J e. ( TopOn ` X ) ) /\ g e. ( Fil ` X ) ) /\ ( f e. ( UFil ` X ) /\ g C_ f ) ) -> J e. ( TopOn ` X ) )
15 simplr 
 |-  ( ( ( ( X e. UFL /\ J e. ( TopOn ` X ) ) /\ g e. ( Fil ` X ) ) /\ ( f e. ( UFil ` X ) /\ g C_ f ) ) -> g e. ( Fil ` X ) )
16 simprr 
 |-  ( ( ( ( X e. UFL /\ J e. ( TopOn ` X ) ) /\ g e. ( Fil ` X ) ) /\ ( f e. ( UFil ` X ) /\ g C_ f ) ) -> g C_ f )
17 fclsss2 
 |-  ( ( J e. ( TopOn ` X ) /\ g e. ( Fil ` X ) /\ g C_ f ) -> ( J fClus f ) C_ ( J fClus g ) )
18 14 15 16 17 syl3anc 
 |-  ( ( ( ( X e. UFL /\ J e. ( TopOn ` X ) ) /\ g e. ( Fil ` X ) ) /\ ( f e. ( UFil ` X ) /\ g C_ f ) ) -> ( J fClus f ) C_ ( J fClus g ) )
19 ssn0 
 |-  ( ( ( J fClus f ) C_ ( J fClus g ) /\ ( J fClus f ) =/= (/) ) -> ( J fClus g ) =/= (/) )
20 19 ex 
 |-  ( ( J fClus f ) C_ ( J fClus g ) -> ( ( J fClus f ) =/= (/) -> ( J fClus g ) =/= (/) ) )
21 18 20 syl 
 |-  ( ( ( ( X e. UFL /\ J e. ( TopOn ` X ) ) /\ g e. ( Fil ` X ) ) /\ ( f e. ( UFil ` X ) /\ g C_ f ) ) -> ( ( J fClus f ) =/= (/) -> ( J fClus g ) =/= (/) ) )
22 21 expr 
 |-  ( ( ( ( X e. UFL /\ J e. ( TopOn ` X ) ) /\ g e. ( Fil ` X ) ) /\ f e. ( UFil ` X ) ) -> ( g C_ f -> ( ( J fClus f ) =/= (/) -> ( J fClus g ) =/= (/) ) ) )
23 22 impcomd 
 |-  ( ( ( ( X e. UFL /\ J e. ( TopOn ` X ) ) /\ g e. ( Fil ` X ) ) /\ f e. ( UFil ` X ) ) -> ( ( ( J fClus f ) =/= (/) /\ g C_ f ) -> ( J fClus g ) =/= (/) ) )
24 23 rexlimdva 
 |-  ( ( ( X e. UFL /\ J e. ( TopOn ` X ) ) /\ g e. ( Fil ` X ) ) -> ( E. f e. ( UFil ` X ) ( ( J fClus f ) =/= (/) /\ g C_ f ) -> ( J fClus g ) =/= (/) ) )
25 13 24 syl5 
 |-  ( ( ( X e. UFL /\ J e. ( TopOn ` X ) ) /\ g e. ( Fil ` X ) ) -> ( ( A. f e. ( UFil ` X ) ( J fClus f ) =/= (/) /\ E. f e. ( UFil ` X ) g C_ f ) -> ( J fClus g ) =/= (/) ) )
26 12 25 mpan2d 
 |-  ( ( ( X e. UFL /\ J e. ( TopOn ` X ) ) /\ g e. ( Fil ` X ) ) -> ( A. f e. ( UFil ` X ) ( J fClus f ) =/= (/) -> ( J fClus g ) =/= (/) ) )
27 26 ralrimdva 
 |-  ( ( X e. UFL /\ J e. ( TopOn ` X ) ) -> ( A. f e. ( UFil ` X ) ( J fClus f ) =/= (/) -> A. g e. ( Fil ` X ) ( J fClus g ) =/= (/) ) )
28 fclscmp 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Comp <-> A. g e. ( Fil ` X ) ( J fClus g ) =/= (/) ) )
29 28 adantl 
 |-  ( ( X e. UFL /\ J e. ( TopOn ` X ) ) -> ( J e. Comp <-> A. g e. ( Fil ` X ) ( J fClus g ) =/= (/) ) )
30 27 29 sylibrd 
 |-  ( ( X e. UFL /\ J e. ( TopOn ` X ) ) -> ( A. f e. ( UFil ` X ) ( J fClus f ) =/= (/) -> J e. Comp ) )
31 10 30 impbid 
 |-  ( ( X e. UFL /\ J e. ( TopOn ` X ) ) -> ( J e. Comp <-> A. f e. ( UFil ` X ) ( J fClus f ) =/= (/) ) )
32 uffclsflim 
 |-  ( f e. ( UFil ` X ) -> ( J fClus f ) = ( J fLim f ) )
33 32 neeq1d 
 |-  ( f e. ( UFil ` X ) -> ( ( J fClus f ) =/= (/) <-> ( J fLim f ) =/= (/) ) )
34 33 ralbiia 
 |-  ( A. f e. ( UFil ` X ) ( J fClus f ) =/= (/) <-> A. f e. ( UFil ` X ) ( J fLim f ) =/= (/) )
35 31 34 bitrdi 
 |-  ( ( X e. UFL /\ J e. ( TopOn ` X ) ) -> ( J e. Comp <-> A. f e. ( UFil ` X ) ( J fLim f ) =/= (/) ) )