Metamath Proof Explorer

Theorem fclscmp

Description: A space is compact iff every filter clusters. (Contributed by Jeff Hankins, 20-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fclscmp 
|- ( J e. ( TopOn ` X ) -> ( J e. Comp <-> A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 fclscmpi 
 |-  ( ( J e. Comp /\ f e. ( Fil ` U. J ) ) -> ( J fClus f ) =/= (/) )
3 2 ralrimiva 
 |-  ( J e. Comp -> A. f e. ( Fil ` U. J ) ( J fClus f ) =/= (/) )
4 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
5 4 fveq2d 
 |-  ( J e. ( TopOn ` X ) -> ( Fil ` X ) = ( Fil ` U. J ) )
6 5 raleqdv 
 |-  ( J e. ( TopOn ` X ) -> ( A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) <-> A. f e. ( Fil ` U. J ) ( J fClus f ) =/= (/) ) )
7 3 6 imbitrrid 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Comp -> A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) ) )
8 elpwi 
 |-  ( x e. ~P ( Clsd ` J ) -> x C_ ( Clsd ` J ) )
9 vn0 
 |-  _V =/= (/)
10 simpr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x = (/) ) -> x = (/) )
11 10 inteqd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x = (/) ) -> |^| x = |^| (/) )
12 int0 
 |-  |^| (/) = _V
13 11 12 eqtrdi 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x = (/) ) -> |^| x = _V )
14 13 neeq1d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x = (/) ) -> ( |^| x =/= (/) <-> _V =/= (/) ) )
15 9 14 mpbiri 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x = (/) ) -> |^| x =/= (/) )
16 15 a1d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x = (/) ) -> ( A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) -> |^| x =/= (/) ) )
17 ssfii 
 |-  ( x e. _V -> x C_ ( fi ` x ) )
18 17 elv 
 |-  x C_ ( fi ` x )
19 simplrl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> x C_ ( Clsd ` J ) )
20 1 cldss2 
 |-  ( Clsd ` J ) C_ ~P U. J
21 4 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> X = U. J )
22 21 pweqd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> ~P X = ~P U. J )
23 20 22 sseqtrrid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> ( Clsd ` J ) C_ ~P X )
24 19 23 sstrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> x C_ ~P X )
25 simpr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> x =/= (/) )
26 simplrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> -. (/) e. ( fi ` x ) )
27 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
28 27 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> X e. J )
29 fsubbas 
 |-  ( X e. J -> ( ( fi ` x ) e. ( fBas ` X ) <-> ( x C_ ~P X /\ x =/= (/) /\ -. (/) e. ( fi ` x ) ) ) )
30 28 29 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> ( ( fi ` x ) e. ( fBas ` X ) <-> ( x C_ ~P X /\ x =/= (/) /\ -. (/) e. ( fi ` x ) ) ) )
31 24 25 26 30 mpbir3and 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> ( fi ` x ) e. ( fBas ` X ) )
32 ssfg 
 |-  ( ( fi ` x ) e. ( fBas ` X ) -> ( fi ` x ) C_ ( X filGen ( fi ` x ) ) )
33 31 32 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> ( fi ` x ) C_ ( X filGen ( fi ` x ) ) )
34 18 33 sstrid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> x C_ ( X filGen ( fi ` x ) ) )
35 34 sselda 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) /\ y e. x ) -> y e. ( X filGen ( fi ` x ) ) )
36 fclssscls 
 |-  ( y e. ( X filGen ( fi ` x ) ) -> ( J fClus ( X filGen ( fi ` x ) ) ) C_ ( ( cls ` J ) ` y ) )
37 35 36 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) /\ y e. x ) -> ( J fClus ( X filGen ( fi ` x ) ) ) C_ ( ( cls ` J ) ` y ) )
38 19 sselda 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) /\ y e. x ) -> y e. ( Clsd ` J ) )
39 cldcls 
 |-  ( y e. ( Clsd ` J ) -> ( ( cls ` J ) ` y ) = y )
40 38 39 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) /\ y e. x ) -> ( ( cls ` J ) ` y ) = y )
41 37 40 sseqtrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) /\ y e. x ) -> ( J fClus ( X filGen ( fi ` x ) ) ) C_ y )
42 41 ralrimiva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> A. y e. x ( J fClus ( X filGen ( fi ` x ) ) ) C_ y )
43 ssint 
 |-  ( ( J fClus ( X filGen ( fi ` x ) ) ) C_ |^| x <-> A. y e. x ( J fClus ( X filGen ( fi ` x ) ) ) C_ y )
44 42 43 sylibr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> ( J fClus ( X filGen ( fi ` x ) ) ) C_ |^| x )
45 fgcl 
 |-  ( ( fi ` x ) e. ( fBas ` X ) -> ( X filGen ( fi ` x ) ) e. ( Fil ` X ) )
46 oveq2 
 |-  ( f = ( X filGen ( fi ` x ) ) -> ( J fClus f ) = ( J fClus ( X filGen ( fi ` x ) ) ) )
47 46 neeq1d 
 |-  ( f = ( X filGen ( fi ` x ) ) -> ( ( J fClus f ) =/= (/) <-> ( J fClus ( X filGen ( fi ` x ) ) ) =/= (/) ) )
48 47 rspcv 
 |-  ( ( X filGen ( fi ` x ) ) e. ( Fil ` X ) -> ( A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) -> ( J fClus ( X filGen ( fi ` x ) ) ) =/= (/) ) )
49 31 45 48 3syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> ( A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) -> ( J fClus ( X filGen ( fi ` x ) ) ) =/= (/) ) )
50 ssn0 
 |-  ( ( ( J fClus ( X filGen ( fi ` x ) ) ) C_ |^| x /\ ( J fClus ( X filGen ( fi ` x ) ) ) =/= (/) ) -> |^| x =/= (/) )
51 44 49 50 syl6an 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) /\ x =/= (/) ) -> ( A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) -> |^| x =/= (/) ) )
52 16 51 pm2.61dane 
 |-  ( ( J e. ( TopOn ` X ) /\ ( x C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` x ) ) ) -> ( A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) -> |^| x =/= (/) ) )
53 52 expr 
 |-  ( ( J e. ( TopOn ` X ) /\ x C_ ( Clsd ` J ) ) -> ( -. (/) e. ( fi ` x ) -> ( A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) -> |^| x =/= (/) ) ) )
54 8 53 sylan2 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. ~P ( Clsd ` J ) ) -> ( -. (/) e. ( fi ` x ) -> ( A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) -> |^| x =/= (/) ) ) )
55 54 com23 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. ~P ( Clsd ` J ) ) -> ( A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) -> ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )
56 55 ralrimdva 
 |-  ( J e. ( TopOn ` X ) -> ( A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) -> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )
57 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
58 cmpfi 
 |-  ( J e. Top -> ( J e. Comp <-> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )
59 57 58 syl 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Comp <-> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )
60 56 59 sylibrd 
 |-  ( J e. ( TopOn ` X ) -> ( A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) -> J e. Comp ) )
61 7 60 impbid 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Comp <-> A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) ) )