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 )