Metamath Proof Explorer


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 ∧ ∀ 𝑥𝑋𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧𝐽 ( 𝑥𝑧𝑥 ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ) )