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 ⊢ X = ⋃ J
Assertion is1stc ⊢ J ∈ 1 st 𝜔 ↔ J ∈ Top ∧ ∀ x ∈ X ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → x ∈ ⋃ y ∩ 𝒫 z

Proof

Step Hyp Ref Expression
1 is1stc.1 ⊢ X = ⋃ J
2 unieq ⊢ j = J → ⋃ j = ⋃ J
3 2 1 eqtr4di ⊢ j = J → ⋃ j = X
4 pweq ⊢ j = J → 𝒫 j = 𝒫 J
5 raleq ⊢ j = J → ∀ z ∈ j x ∈ z → x ∈ ⋃ y ∩ 𝒫 z ↔ ∀ z ∈ J x ∈ z → x ∈ ⋃ y ∩ 𝒫 z
6 5 anbi2d ⊢ j = J → y ≼ ω ∧ ∀ z ∈ j x ∈ z → x ∈ ⋃ y ∩ 𝒫 z ↔ y ≼ ω ∧ ∀ z ∈ J x ∈ z → x ∈ ⋃ y ∩ 𝒫 z
7 4 6 rexeqbidv ⊢ j = J → ∃ y ∈ 𝒫 j y ≼ ω ∧ ∀ z ∈ j x ∈ z → x ∈ ⋃ y ∩ 𝒫 z ↔ ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → x ∈ ⋃ y ∩ 𝒫 z
8 3 7 raleqbidv ⊢ j = J → ∀ x ∈ ⋃ j ∃ y ∈ 𝒫 j y ≼ ω ∧ ∀ z ∈ j x ∈ z → x ∈ ⋃ y ∩ 𝒫 z ↔ ∀ x ∈ X ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → x ∈ ⋃ y ∩ 𝒫 z
9 df-1stc ⊢ 1 st 𝜔 = j ∈ Top | ∀ x ∈ ⋃ j ∃ y ∈ 𝒫 j y ≼ ω ∧ ∀ z ∈ j x ∈ z → x ∈ ⋃ y ∩ 𝒫 z
10 8 9 elrab2 ⊢ J ∈ 1 st 𝜔 ↔ J ∈ Top ∧ ∀ x ∈ X ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → x ∈ ⋃ y ∩ 𝒫 z