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

Metamath Proof Explorer

Theorem alexsubALTlem1

Description: Lemma for alexsubALT . A compact space has a subbase such that every cover taken from it has a finite subcover. (Contributed by Jeff Hankins, 27-Jan-2010)

Ref Expression
Hypothesis alexsubALT.1 ⊢ 𝑋 = ∪ 𝐽
Assertion alexsubALTlem1 ( 𝐽 ∈ Comp → ∃ 𝑥 ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )

Proof

Step Hyp Ref Expression
1 alexsubALT.1 ⊢ 𝑋 = ∪ 𝐽
2 cmptop ⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
3 fitop ⊢ ( 𝐽 ∈ Top → ( fi ‘ 𝐽 ) = 𝐽 )
4 3 fveq2d ⊢ ( 𝐽 ∈ Top → ( topGen ‘ ( fi ‘ 𝐽 ) ) = ( topGen ‘ 𝐽 ) )
5 tgtop ⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )
6 4 5 eqtr2d ⊢ ( 𝐽 ∈ Top → 𝐽 = ( topGen ‘ ( fi ‘ 𝐽 ) ) )
7 2 6 syl ⊢ ( 𝐽 ∈ Comp → 𝐽 = ( topGen ‘ ( fi ‘ 𝐽 ) ) )
8 velpw ⊢ ( 𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽 )
9 1 cmpcov ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 )
10 9 3exp ⊢ ( 𝐽 ∈ Comp → ( 𝑐 ⊆ 𝐽 → ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
11 8 10 biimtrid ⊢ ( 𝐽 ∈ Comp → ( 𝑐 ∈ 𝒫 𝐽 → ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
12 11 ralrimiv ⊢ ( 𝐽 ∈ Comp → ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) )
13 2fveq3 ⊢ ( 𝑥 = 𝐽 → ( topGen ‘ ( fi ‘ 𝑥 ) ) = ( topGen ‘ ( fi ‘ 𝐽 ) ) )
14 13 eqeq2d ⊢ ( 𝑥 = 𝐽 → ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ↔ 𝐽 = ( topGen ‘ ( fi ‘ 𝐽 ) ) ) )
15 pweq ⊢ ( 𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽 )
16 15 raleqdv ⊢ ( 𝑥 = 𝐽 → ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
17 14 16 anbi12d ⊢ ( 𝑥 = 𝐽 → ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ↔ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝐽 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) )
18 17 spcegv ⊢ ( 𝐽 ∈ Comp → ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝐽 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑥 ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) )
19 7 12 18 mp2and ⊢ ( 𝐽 ∈ Comp → ∃ 𝑥 ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )