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∈1st𝜔∧A∈X→∃x∈𝒫Jx≼ω∧∀y∈JA∈y→∃z∈xA∈z∧z⊆y

Proof

Step Hyp Ref Expression
1 1stcclb.1 ⊢X=⋃J
2 1 is1stc2 ⊢J∈1st𝜔↔J∈Top∧∀w∈X∃x∈𝒫Jx≼ω∧∀y∈Jw∈y→∃z∈xw∈z∧z⊆y
3 2 simprbi ⊢J∈1st𝜔→∀w∈X∃x∈𝒫Jx≼ω∧∀y∈Jw∈y→∃z∈xw∈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∈xw∈z∧z⊆y↔∃z∈xA∈z∧z⊆y
8 4 7 imbi12d ⊢w=A→w∈y→∃z∈xw∈z∧z⊆y↔A∈y→∃z∈xA∈z∧z⊆y
9 8 ralbidv ⊢w=A→∀y∈Jw∈y→∃z∈xw∈z∧z⊆y↔∀y∈JA∈y→∃z∈xA∈z∧z⊆y
10 9 anbi2d ⊢w=A→x≼ω∧∀y∈Jw∈y→∃z∈xw∈z∧z⊆y↔x≼ω∧∀y∈JA∈y→∃z∈xA∈z∧z⊆y
11 10 rexbidv ⊢w=A→∃x∈𝒫Jx≼ω∧∀y∈Jw∈y→∃z∈xw∈z∧z⊆y↔∃x∈𝒫Jx≼ω∧∀y∈JA∈y→∃z∈xA∈z∧z⊆y
12 11 rspcv ⊢A∈X→∀w∈X∃x∈𝒫Jx≼ω∧∀y∈Jw∈y→∃z∈xw∈z∧z⊆y→∃x∈𝒫Jx≼ω∧∀y∈JA∈y→∃z∈xA∈z∧z⊆y
13 3 12 mpan9 ⊢J∈1st𝜔∧A∈X→∃x∈𝒫Jx≼ω∧∀y∈JA∈y→∃z∈xA∈z∧z⊆y