is1stc

Description: The predicate "is a first-countable topology." This can be described as "every point has a countable local basis" - that is, every point has a countable collection of open sets containing it such that every open set containing the point has an open set from this collection as a subset. (Contributed by Jeff Hankins, 22-Aug-2009)

		Ref	Expression
	Hypothesis	is1stc.1	$⊢ X = ⋃ J$
	Assertion	is1stc	$⊢ J \in 1^{st} 𝜔 \leftrightarrow (J \in Top \land \forall x \in X \exists y \in 𝒫 J (y ≼ ω \land \forall z \in J (x \in z \to x \in ⋃ (y \cap 𝒫 z))))$

Proof

Step	Hyp	Ref	Expression
1		is1stc.1	$⊢ X = ⋃ J$
2		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
3	2 1	eqtr4di	$⊢ j = J \to ⋃ j = X$
4		pweq	$⊢ j = J \to 𝒫 j = 𝒫 J$
5		raleq	$⊢ j = J \to (\forall z \in j (x \in z \to x \in ⋃ (y \cap 𝒫 z)) \leftrightarrow \forall z \in J (x \in z \to x \in ⋃ (y \cap 𝒫 z)))$
6	5	anbi2d	$⊢ j = J \to ((y ≼ ω \land \forall z \in j (x \in z \to x \in ⋃ (y \cap 𝒫 z))) \leftrightarrow (y ≼ ω \land \forall z \in J (x \in z \to x \in ⋃ (y \cap 𝒫 z))))$
7	4 6	rexeqbidv	$⊢ j = J \to (\exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to x \in ⋃ (y \cap 𝒫 z))) \leftrightarrow \exists y \in 𝒫 J (y ≼ ω \land \forall z \in J (x \in z \to x \in ⋃ (y \cap 𝒫 z))))$
8	3 7	raleqbidv	$⊢ j = J \to (\forall x \in ⋃ j \exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to x \in ⋃ (y \cap 𝒫 z))) \leftrightarrow \forall x \in X \exists y \in 𝒫 J (y ≼ ω \land \forall z \in J (x \in z \to x \in ⋃ (y \cap 𝒫 z))))$
9		df-1stc	$⊢ 1^{st} 𝜔 = \{j \in Top \| \forall x \in ⋃ j \exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to x \in ⋃ (y \cap 𝒫 z)))\}$
10	8 9	elrab2	$⊢ J \in 1^{st} 𝜔 \leftrightarrow (J \in Top \land \forall x \in X \exists y \in 𝒫 J (y ≼ ω \land \forall z \in J (x \in z \to x \in ⋃ (y \cap 𝒫 z))))$

Metamath Proof Explorer

Theorem is1stc

Proof