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 ⊢ X = ⋃ J
Assertion alexsubALTlem1 ⊢ J ∈ Comp → ∃ x J = topGen ⁡ fi ⁡ x ∧ ∀ c ∈ 𝒫 x X = ⋃ c → ∃ d ∈ 𝒫 c ∩ Fin X = ⋃ d

Proof

Step Hyp Ref Expression
1 alexsubALT.1 ⊢ X = ⋃ J
2 cmptop ⊢ J ∈ Comp → J ∈ Top
3 fitop ⊢ J ∈ Top → fi ⁡ J = J
4 3 fveq2d ⊢ J ∈ Top → topGen ⁡ fi ⁡ J = topGen ⁡ J
5 tgtop ⊢ J ∈ Top → topGen ⁡ J = J
6 4 5 eqtr2d ⊢ J ∈ Top → J = topGen ⁡ fi ⁡ J
7 2 6 syl ⊢ J ∈ Comp → J = topGen ⁡ fi ⁡ J
8 velpw ⊢ c ∈ 𝒫 J ↔ c ⊆ J
9 1 cmpcov ⊢ J ∈ Comp ∧ c ⊆ J ∧ X = ⋃ c → ∃ d ∈ 𝒫 c ∩ Fin X = ⋃ d
10 9 3exp ⊢ J ∈ Comp → c ⊆ J → X = ⋃ c → ∃ d ∈ 𝒫 c ∩ Fin X = ⋃ d
11 8 10 syl5bi ⊢ J ∈ Comp → c ∈ 𝒫 J → X = ⋃ c → ∃ d ∈ 𝒫 c ∩ Fin X = ⋃ d
12 11 ralrimiv ⊢ J ∈ Comp → ∀ c ∈ 𝒫 J X = ⋃ c → ∃ d ∈ 𝒫 c ∩ Fin X = ⋃ d
13 2fveq3 ⊢ x = J → topGen ⁡ fi ⁡ x = topGen ⁡ fi ⁡ J
14 13 eqeq2d ⊢ x = J → J = topGen ⁡ fi ⁡ x ↔ J = topGen ⁡ fi ⁡ J
15 pweq ⊢ x = J → 𝒫 x = 𝒫 J
16 15 raleqdv ⊢ x = J → ∀ c ∈ 𝒫 x X = ⋃ c → ∃ d ∈ 𝒫 c ∩ Fin X = ⋃ d ↔ ∀ c ∈ 𝒫 J X = ⋃ c → ∃ d ∈ 𝒫 c ∩ Fin X = ⋃ d
17 14 16 anbi12d ⊢ x = J → J = topGen ⁡ fi ⁡ x ∧ ∀ c ∈ 𝒫 x X = ⋃ c → ∃ d ∈ 𝒫 c ∩ Fin X = ⋃ d ↔ J = topGen ⁡ fi ⁡ J ∧ ∀ c ∈ 𝒫 J X = ⋃ c → ∃ d ∈ 𝒫 c ∩ Fin X = ⋃ d
18 17 spcegv ⊢ J ∈ Comp → J = topGen ⁡ fi ⁡ J ∧ ∀ c ∈ 𝒫 J X = ⋃ c → ∃ d ∈ 𝒫 c ∩ Fin X = ⋃ d → ∃ x J = topGen ⁡ fi ⁡ x ∧ ∀ c ∈ 𝒫 x X = ⋃ c → ∃ d ∈ 𝒫 c ∩ Fin X = ⋃ d
19 7 12 18 mp2and ⊢ J ∈ Comp → ∃ x J = topGen ⁡ fi ⁡ x ∧ ∀ c ∈ 𝒫 x X = ⋃ c → ∃ d ∈ 𝒫 c ∩ Fin X = ⋃ d