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