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