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 \in Top \| \forall y \in (𝒫 ⋃ x ∖ Fin) \exists z \in ⋃ x z \in limPt (x) (y)\}$
	Assertion	pibp21	$⊢ J \in W \leftrightarrow (J \in Top \land \forall y \in (𝒫 X ∖ Fin) \exists z \in X z \in limPt (J) (y))$

Proof

Step	Hyp	Ref	Expression
1		pibp21.x	$⊢ X = ⋃ J$
2		pibp21.21	$⊢ W = \{x \in Top \| \forall y \in (𝒫 ⋃ x ∖ Fin) \exists z \in ⋃ x z \in limPt (x) (y)\}$
3		unieq	$⊢ x = J \to ⋃ x = ⋃ J$
4	3 1	eqtr4di	$⊢ x = J \to ⋃ x = X$
5	4	pweqd	$⊢ x = J \to 𝒫 ⋃ x = 𝒫 X$
6	5	difeq1d	$⊢ x = J \to 𝒫 ⋃ x ∖ Fin = 𝒫 X ∖ Fin$
7		fveq2	$⊢ x = J \to limPt (x) = limPt (J)$
8	7	fveq1d	$⊢ x = J \to limPt (x) (y) = limPt (J) (y)$
9	8	eleq2d	$⊢ x = J \to (z \in limPt (x) (y) \leftrightarrow z \in limPt (J) (y))$
10	4 9	rexeqbidv	$⊢ x = J \to (\exists z \in ⋃ x z \in limPt (x) (y) \leftrightarrow \exists z \in X z \in limPt (J) (y))$
11	6 10	raleqbidv	$⊢ x = J \to (\forall y \in (𝒫 ⋃ x ∖ Fin) \exists z \in ⋃ x z \in limPt (x) (y) \leftrightarrow \forall y \in (𝒫 X ∖ Fin) \exists z \in X z \in limPt (J) (y))$
12	11 2	elrab2	$⊢ J \in W \leftrightarrow (J \in Top \land \forall y \in (𝒫 X ∖ Fin) \exists z \in X z \in limPt (J) (y))$