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 ⊢ ( 𝜑 → 𝑋 ∈ UFL )
alexsub.2 ⊢ ( 𝜑 → 𝑋 = ∪ 𝐵 )
alexsub.3 ⊢ ( 𝜑 → 𝐽 = ( topGen ‘ ( fi ‘ 𝐵 ) ) )
alexsub.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 )
Assertion alexsub ( 𝜑 → 𝐽 ∈ Comp )

Proof

Step Hyp Ref Expression
1 alexsub.1 ⊢ ( 𝜑 → 𝑋 ∈ UFL )
2 alexsub.2 ⊢ ( 𝜑 → 𝑋 = ∪ 𝐵 )
3 alexsub.3 ⊢ ( 𝜑 → 𝐽 = ( topGen ‘ ( fi ‘ 𝐵 ) ) )
4 alexsub.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 )
5 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → 𝑋 ∈ UFL )
6 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → 𝑋 = ∪ 𝐵 )
7 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → 𝐽 = ( topGen ‘ ( fi ‘ 𝐵 ) ) )
8 4 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 )
9 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → 𝑓 ∈ ( UFil ‘ 𝑋 ) )
10 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → ( 𝐽 fLim 𝑓 ) = ∅ )
11 5 6 7 8 9 10 alexsublem ⊢ ¬ ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) )
12 11 pm2.21i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → ¬ ( 𝐽 fLim 𝑓 ) = ∅ )
13 12 expr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( ( 𝐽 fLim 𝑓 ) = ∅ → ¬ ( 𝐽 fLim 𝑓 ) = ∅ ) )
14 13 pm2.01d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ¬ ( 𝐽 fLim 𝑓 ) = ∅ )
15 14 neqned ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( 𝐽 fLim 𝑓 ) ≠ ∅ )
16 15 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ )
17 fibas ⊢ ( fi ‘ 𝐵 ) ∈ TopBases
18 tgtopon ⊢ ( ( fi ‘ 𝐵 ) ∈ TopBases → ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) )
19 17 18 ax-mp ⊢ ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) )
20 3 19 eqeltrdi ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) )
21 1 elexd ⊢ ( 𝜑 → 𝑋 ∈ V )
22 2 21 eqeltrrd ⊢ ( 𝜑 → ∪ 𝐵 ∈ V )
23 uniexb ⊢ ( 𝐵 ∈ V ↔ ∪ 𝐵 ∈ V )
24 22 23 sylibr ⊢ ( 𝜑 → 𝐵 ∈ V )
25 fiuni ⊢ ( 𝐵 ∈ V → ∪ 𝐵 = ∪ ( fi ‘ 𝐵 ) )
26 24 25 syl ⊢ ( 𝜑 → ∪ 𝐵 = ∪ ( fi ‘ 𝐵 ) )
27 2 26 eqtrd ⊢ ( 𝜑 → 𝑋 = ∪ ( fi ‘ 𝐵 ) )
28 27 fveq2d ⊢ ( 𝜑 → ( TopOn ‘ 𝑋 ) = ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) )
29 20 28 eleqtrrd ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
30 ufilcmp ⊢ ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽 ∈ Comp ↔ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )
31 1 29 30 syl2anc ⊢ ( 𝜑 → ( 𝐽 ∈ Comp ↔ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )
32 16 31 mpbird ⊢ ( 𝜑 → 𝐽 ∈ Comp )