This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem alexsub

Description: The Alexander Subbase Theorem: If B is a subbase for the topology J , and any cover taken from B has a finite subcover, then the generated topology is compact. This proof uses the ultrafilter lemma; see alexsubALT for a proof using Zorn's lemma. (Contributed by Jeff Hankins, 24-Jan-2010) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses alexsub.1 
|- ( ph -> X e. UFL )
alexsub.2 
|- ( ph -> X = U. B )
alexsub.3 
|- ( ph -> J = ( topGen ` ( fi ` B ) ) )
alexsub.4 
|- ( ( ph /\ ( x C_ B /\ X = U. x ) ) -> E. y e. ( ~P x i^i Fin ) X = U. y )
Assertion alexsub 
|- ( ph -> J e. Comp )

Proof

Step Hyp Ref Expression
1 alexsub.1 
 |-  ( ph -> X e. UFL )
2 alexsub.2 
 |-  ( ph -> X = U. B )
3 alexsub.3 
 |-  ( ph -> J = ( topGen ` ( fi ` B ) ) )
4 alexsub.4 
 |-  ( ( ph /\ ( x C_ B /\ X = U. x ) ) -> E. y e. ( ~P x i^i Fin ) X = U. y )
5 1 adantr 
 |-  ( ( ph /\ ( f e. ( UFil ` X ) /\ ( J fLim f ) = (/) ) ) -> X e. UFL )
6 2 adantr 
 |-  ( ( ph /\ ( f e. ( UFil ` X ) /\ ( J fLim f ) = (/) ) ) -> X = U. B )
7 3 adantr 
 |-  ( ( ph /\ ( f e. ( UFil ` X ) /\ ( J fLim f ) = (/) ) ) -> J = ( topGen ` ( fi ` B ) ) )
8 4 adantlr 
 |-  ( ( ( ph /\ ( f e. ( UFil ` X ) /\ ( J fLim f ) = (/) ) ) /\ ( x C_ B /\ X = U. x ) ) -> E. y e. ( ~P x i^i Fin ) X = U. y )
9 simprl 
 |-  ( ( ph /\ ( f e. ( UFil ` X ) /\ ( J fLim f ) = (/) ) ) -> f e. ( UFil ` X ) )
10 simprr 
 |-  ( ( ph /\ ( f e. ( UFil ` X ) /\ ( J fLim f ) = (/) ) ) -> ( J fLim f ) = (/) )
11 5 6 7 8 9 10 alexsublem 
 |-  -. ( ph /\ ( f e. ( UFil ` X ) /\ ( J fLim f ) = (/) ) )
12 11 pm2.21i 
 |-  ( ( ph /\ ( f e. ( UFil ` X ) /\ ( J fLim f ) = (/) ) ) -> -. ( J fLim f ) = (/) )
13 12 expr 
 |-  ( ( ph /\ f e. ( UFil ` X ) ) -> ( ( J fLim f ) = (/) -> -. ( J fLim f ) = (/) ) )
14 13 pm2.01d 
 |-  ( ( ph /\ f e. ( UFil ` X ) ) -> -. ( J fLim f ) = (/) )
15 14 neqned 
 |-  ( ( ph /\ f e. ( UFil ` X ) ) -> ( J fLim f ) =/= (/) )
16 15 ralrimiva 
 |-  ( ph -> A. f e. ( UFil ` X ) ( J fLim f ) =/= (/) )
17 fibas 
 |-  ( fi ` B ) e. TopBases
18 tgtopon 
 |-  ( ( fi ` B ) e. TopBases -> ( topGen ` ( fi ` B ) ) e. ( TopOn ` U. ( fi ` B ) ) )
19 17 18 ax-mp 
 |-  ( topGen ` ( fi ` B ) ) e. ( TopOn ` U. ( fi ` B ) )
20 3 19 eqeltrdi 
 |-  ( ph -> J e. ( TopOn ` U. ( fi ` B ) ) )
21 1 elexd 
 |-  ( ph -> X e. _V )
22 2 21 eqeltrrd 
 |-  ( ph -> U. B e. _V )
23 uniexb 
 |-  ( B e. _V <-> U. B e. _V )
24 22 23 sylibr 
 |-  ( ph -> B e. _V )
25 fiuni 
 |-  ( B e. _V -> U. B = U. ( fi ` B ) )
26 24 25 syl 
 |-  ( ph -> U. B = U. ( fi ` B ) )
27 2 26 eqtrd 
 |-  ( ph -> X = U. ( fi ` B ) )
28 27 fveq2d 
 |-  ( ph -> ( TopOn ` X ) = ( TopOn ` U. ( fi ` B ) ) )
29 20 28 eleqtrrd 
 |-  ( ph -> J e. ( TopOn ` X ) )
30 ufilcmp 
 |-  ( ( X e. UFL /\ J e. ( TopOn ` X ) ) -> ( J e. Comp <-> A. f e. ( UFil ` X ) ( J fLim f ) =/= (/) ) )
31 1 29 30 syl2anc 
 |-  ( ph -> ( J e. Comp <-> A. f e. ( UFil ` X ) ( J fLim f ) =/= (/) ) )
32 16 31 mpbird 
 |-  ( ph -> J e. Comp )