Metamath Proof Explorer

Theorem pibt1

Description: Theorem T000001 of pi-base. A compact topology is also countably compact. See pibp16 and pibp19 for the definitions of the relevant properties. (Contributed by ML, 8-Dec-2020)

Ref Expression
Hypothesis pibt1.19 ⊢ C = x ∈ Top | ∀ y ∈ 𝒫 x ⋃ x = ⋃ y ∧ y ≼ ω → ∃ z ∈ 𝒫 y ∩ Fin ⋃ x = ⋃ z
Assertion pibt1 ⊢ J ∈ Comp → J ∈ C

Proof

Step Hyp Ref Expression
1 pibt1.19 ⊢ C = x ∈ Top | ∀ y ∈ 𝒫 x ⋃ x = ⋃ y ∧ y ≼ ω → ∃ z ∈ 𝒫 y ∩ Fin ⋃ x = ⋃ z
2 pm3.41 ⊢ ⋃ J = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z → ⋃ J = ⋃ y ∧ y ≼ ω → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z
3 2 ralimi ⊢ ∀ y ∈ 𝒫 J ⋃ J = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z → ∀ y ∈ 𝒫 J ⋃ J = ⋃ y ∧ y ≼ ω → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z
4 3 anim2i ⊢ J ∈ Top ∧ ∀ y ∈ 𝒫 J ⋃ J = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z → J ∈ Top ∧ ∀ y ∈ 𝒫 J ⋃ J = ⋃ y ∧ y ≼ ω → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z
5 eqid ⊢ ⋃ J = ⋃ J
6 5 pibp16 ⊢ J ∈ Comp ↔ J ∈ Top ∧ ∀ y ∈ 𝒫 J ⋃ J = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z
7 5 1 pibp19 ⊢ J ∈ C ↔ J ∈ Top ∧ ∀ y ∈ 𝒫 J ⋃ J = ⋃ y ∧ y ≼ ω → ∃ z ∈ 𝒫 y ∩ Fin ⋃ J = ⋃ z
8 4 6 7 3imtr4i ⊢ J ∈ Comp → J ∈ C