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	⊢ 𝑋 = ∪ 𝐽
	pibp21.21	⊢ 𝑊 = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∖ Fin ) ∃ 𝑧 ∈ ∪ 𝑥 𝑧 ∈ ( ( limPt ‘ 𝑥 ) ‘ 𝑦 ) }
Assertion	pibp21	⊢ ( 𝐽 ∈ 𝑊 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑧 ∈ 𝑋 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pibp21.x	⊢ 𝑋 = ∪ 𝐽
2		pibp21.21	⊢ 𝑊 = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∖ Fin ) ∃ 𝑧 ∈ ∪ 𝑥 𝑧 ∈ ( ( limPt ‘ 𝑥 ) ‘ 𝑦 ) }
3		unieq	⊢ ( 𝑥 = 𝐽 → ∪ 𝑥 = ∪ 𝐽 )
4	3 1	eqtr4di	⊢ ( 𝑥 = 𝐽 → ∪ 𝑥 = 𝑋 )
5	4	pweqd	⊢ ( 𝑥 = 𝐽 → 𝒫 ∪ 𝑥 = 𝒫 𝑋 )
6	5	difeq1d	⊢ ( 𝑥 = 𝐽 → ( 𝒫 ∪ 𝑥 ∖ Fin ) = ( 𝒫 𝑋 ∖ Fin ) )
7		fveq2	⊢ ( 𝑥 = 𝐽 → ( limPt ‘ 𝑥 ) = ( limPt ‘ 𝐽 ) )
8	7	fveq1d	⊢ ( 𝑥 = 𝐽 → ( ( limPt ‘ 𝑥 ) ‘ 𝑦 ) = ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) )
9	8	eleq2d	⊢ ( 𝑥 = 𝐽 → ( 𝑧 ∈ ( ( limPt ‘ 𝑥 ) ‘ 𝑦 ) ↔ 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ) )
10	4 9	rexeqbidv	⊢ ( 𝑥 = 𝐽 → ( ∃ 𝑧 ∈ ∪ 𝑥 𝑧 ∈ ( ( limPt ‘ 𝑥 ) ‘ 𝑦 ) ↔ ∃ 𝑧 ∈ 𝑋 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ) )
11	6 10	raleqbidv	⊢ ( 𝑥 = 𝐽 → ( ∀ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∖ Fin ) ∃ 𝑧 ∈ ∪ 𝑥 𝑧 ∈ ( ( limPt ‘ 𝑥 ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑧 ∈ 𝑋 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ) )
12	11 2	elrab2	⊢ ( 𝐽 ∈ 𝑊 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑧 ∈ 𝑋 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ) )