Metamath Proof Explorer

Theorem 1stcclb

Description: A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009)

Ref Expression
Hypothesis 1stcclb.1 ⊢ X = ⋃ J
Assertion 1stcclb ⊢ J ∈ 1 st 𝜔 ∧ A ∈ X → ∃ x ∈ 𝒫 J x ≼ ω ∧ ∀ y ∈ J A ∈ y → ∃ z ∈ x A ∈ z ∧ z ⊆ y

Proof

Step Hyp Ref Expression
1 1stcclb.1 ⊢ X = ⋃ J
2 1 is1stc2 ⊢ J ∈ 1 st 𝜔 ↔ J ∈ Top ∧ ∀ w ∈ X ∃ x ∈ 𝒫 J x ≼ ω ∧ ∀ y ∈ J w ∈ y → ∃ z ∈ x w ∈ z ∧ z ⊆ y
3 2 simprbi ⊢ J ∈ 1 st 𝜔 → ∀ w ∈ X ∃ x ∈ 𝒫 J x ≼ ω ∧ ∀ y ∈ J w ∈ y → ∃ z ∈ x w ∈ z ∧ z ⊆ y
4 eleq1 ⊢ w = A → w ∈ y ↔ A ∈ y
5 eleq1 ⊢ w = A → w ∈ z ↔ A ∈ z
6 5 anbi1d ⊢ w = A → w ∈ z ∧ z ⊆ y ↔ A ∈ z ∧ z ⊆ y
7 6 rexbidv ⊢ w = A → ∃ z ∈ x w ∈ z ∧ z ⊆ y ↔ ∃ z ∈ x A ∈ z ∧ z ⊆ y
8 4 7 imbi12d ⊢ w = A → w ∈ y → ∃ z ∈ x w ∈ z ∧ z ⊆ y ↔ A ∈ y → ∃ z ∈ x A ∈ z ∧ z ⊆ y
9 8 ralbidv ⊢ w = A → ∀ y ∈ J w ∈ y → ∃ z ∈ x w ∈ z ∧ z ⊆ y ↔ ∀ y ∈ J A ∈ y → ∃ z ∈ x A ∈ z ∧ z ⊆ y
10 9 anbi2d ⊢ w = A → x ≼ ω ∧ ∀ y ∈ J w ∈ y → ∃ z ∈ x w ∈ z ∧ z ⊆ y ↔ x ≼ ω ∧ ∀ y ∈ J A ∈ y → ∃ z ∈ x A ∈ z ∧ z ⊆ y
11 10 rexbidv ⊢ w = A → ∃ x ∈ 𝒫 J x ≼ ω ∧ ∀ y ∈ J w ∈ y → ∃ z ∈ x w ∈ z ∧ z ⊆ y ↔ ∃ x ∈ 𝒫 J x ≼ ω ∧ ∀ y ∈ J A ∈ y → ∃ z ∈ x A ∈ z ∧ z ⊆ y
12 11 rspcv ⊢ A ∈ X → ∀ w ∈ X ∃ x ∈ 𝒫 J x ≼ ω ∧ ∀ y ∈ J w ∈ y → ∃ z ∈ x w ∈ z ∧ z ⊆ y → ∃ x ∈ 𝒫 J x ≼ ω ∧ ∀ y ∈ J A ∈ y → ∃ z ∈ x A ∈ z ∧ z ⊆ y
13 3 12 mpan9 ⊢ J ∈ 1 st 𝜔 ∧ A ∈ X → ∃ x ∈ 𝒫 J x ≼ ω ∧ ∀ y ∈ J A ∈ y → ∃ z ∈ x A ∈ z ∧ z ⊆ y