Metamath Proof Explorer

Theorem pibp21

Description: Property P000021 of pi-base. The class of weakly countably compact topologies, or limit point compact topologies. A space X is weakly countably compact if every infinite subset of X has a limit point. (Contributed by ML, 9-Dec-2020)

Ref Expression
Hypotheses pibp21.x ⊢ X = ⋃ J
pibp21.21 ⊢ W = x ∈ Top | ∀ y ∈ 𝒫 ⋃ x ∖ Fin ∃ z ∈ ⋃ x z ∈ limPt ⁡ x ⁡ y
Assertion pibp21 ⊢ J ∈ W ↔ J ∈ Top ∧ ∀ y ∈ 𝒫 X ∖ Fin ∃ z ∈ X z ∈ limPt ⁡ J ⁡ y

Proof

Step Hyp Ref Expression
1 pibp21.x ⊢ X = ⋃ J
2 pibp21.21 ⊢ W = x ∈ Top | ∀ y ∈ 𝒫 ⋃ x ∖ Fin ∃ z ∈ ⋃ x z ∈ limPt ⁡ x ⁡ y
3 unieq ⊢ x = J → ⋃ x = ⋃ J
4 3 1 eqtr4di ⊢ x = J → ⋃ x = X
5 4 pweqd ⊢ x = J → 𝒫 ⋃ x = 𝒫 X
6 5 difeq1d ⊢ x = J → 𝒫 ⋃ x ∖ Fin = 𝒫 X ∖ Fin
7 fveq2 ⊢ x = J → limPt ⁡ x = limPt ⁡ J
8 7 fveq1d ⊢ x = J → limPt ⁡ x ⁡ y = limPt ⁡ J ⁡ y
9 8 eleq2d ⊢ x = J → z ∈ limPt ⁡ x ⁡ y ↔ z ∈ limPt ⁡ J ⁡ y
10 4 9 rexeqbidv ⊢ x = J → ∃ z ∈ ⋃ x z ∈ limPt ⁡ x ⁡ y ↔ ∃ z ∈ X z ∈ limPt ⁡ J ⁡ y
11 6 10 raleqbidv ⊢ x = J → ∀ y ∈ 𝒫 ⋃ x ∖ Fin ∃ z ∈ ⋃ x z ∈ limPt ⁡ x ⁡ y ↔ ∀ y ∈ 𝒫 X ∖ Fin ∃ z ∈ X z ∈ limPt ⁡ J ⁡ y
12 11 2 elrab2 ⊢ J ∈ W ↔ J ∈ Top ∧ ∀ y ∈ 𝒫 X ∖ Fin ∃ z ∈ X z ∈ limPt ⁡ J ⁡ y