This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
Assertion 1stcclb ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝒫 𝐽 ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 1stcclb.1 ⊢ 𝑋 = ∪ 𝐽
2 1 is1stc2 ⊢ ( 𝐽 ∈ 1stω ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑤 ∈ 𝑋 ∃ 𝑥 ∈ 𝒫 𝐽 ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑤 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ) )
3 2 simprbi ⊢ ( 𝐽 ∈ 1stω → ∀ 𝑤 ∈ 𝑋 ∃ 𝑥 ∈ 𝒫 𝐽 ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑤 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) )
4 eleq1 ⊢ ( 𝑤 = 𝐴 → ( 𝑤 ∈ 𝑦 ↔ 𝐴 ∈ 𝑦 ) )
5 eleq1 ⊢ ( 𝑤 = 𝐴 → ( 𝑤 ∈ 𝑧 ↔ 𝐴 ∈ 𝑧 ) )
6 5 anbi1d ⊢ ( 𝑤 = 𝐴 → ( ( 𝑤 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ↔ ( 𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) )
7 6 rexbidv ⊢ ( 𝑤 = 𝐴 → ( ∃ 𝑧 ∈ 𝑥 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ↔ ∃ 𝑧 ∈ 𝑥 ( 𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) )
8 4 7 imbi12d ⊢ ( 𝑤 = 𝐴 → ( ( 𝑤 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ↔ ( 𝐴 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) )
9 8 ralbidv ⊢ ( 𝑤 = 𝐴 → ( ∀ 𝑦 ∈ 𝐽 ( 𝑤 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) )
10 9 anbi2d ⊢ ( 𝑤 = 𝐴 → ( ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑤 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ↔ ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ) )
11 10 rexbidv ⊢ ( 𝑤 = 𝐴 → ( ∃ 𝑥 ∈ 𝒫 𝐽 ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑤 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ↔ ∃ 𝑥 ∈ 𝒫 𝐽 ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ) )
12 11 rspcv ⊢ ( 𝐴 ∈ 𝑋 → ( ∀ 𝑤 ∈ 𝑋 ∃ 𝑥 ∈ 𝒫 𝐽 ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑤 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) → ∃ 𝑥 ∈ 𝒫 𝐽 ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ) )
13 3 12 mpan9 ⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝒫 𝐽 ( 𝑥 ≼ ω ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑥 ( 𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) )