Theorem 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	⊢ 𝑋 = ∪ 𝐽
Assertion	is1stc	⊢ ( 𝐽 ∈ 1stω ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		is1stc.1	⊢ 𝑋 = ∪ 𝐽
2		unieq	⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
3	2 1	eqtr4di	⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = 𝑋 )
4		pweq	⊢ ( 𝑗 = 𝐽 → 𝒫 𝑗 = 𝒫 𝐽 )
5		raleq	⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) )
6	5	anbi2d	⊢ ( 𝑗 = 𝐽 → ( ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ↔ ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ) )
7	4 6	rexeqbidv	⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ↔ ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ) )
8	3 7	raleqbidv	⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ) )
9		df-1stc	⊢ 1stω = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) }
10	8 9	elrab2	⊢ ( 𝐽 ∈ 1stω ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ) )