Metamath Proof Explorer

Theorem is1stc2

Description: An equivalent way of saying "is a first-countable topology." (Contributed by Jeff Hankins, 22-Aug-2009) (Revised by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis is1stc.1 ⊢X=⋃J
Assertion is1stc2 ⊢J∈1st𝜔↔J∈Top∧∀x∈X∃y∈𝒫Jy≼ω∧∀z∈Jx∈z→∃w∈yx∈w∧w⊆z

Proof

Step Hyp Ref Expression
1 is1stc.1 ⊢X=⋃J
2 1 is1stc ⊢J∈1st𝜔↔J∈Top∧∀x∈X∃y∈𝒫Jy≼ω∧∀z∈Jx∈z→x∈⋃y∩𝒫z
3 elin ⊢w∈y∩𝒫z↔w∈y∧w∈𝒫z
4 velpw ⊢w∈𝒫z↔w⊆z
5 4 anbi2i ⊢w∈y∧w∈𝒫z↔w∈y∧w⊆z
6 3 5 bitri ⊢w∈y∩𝒫z↔w∈y∧w⊆z
7 6 anbi2i ⊢x∈w∧w∈y∩𝒫z↔x∈w∧w∈y∧w⊆z
8 an12 ⊢x∈w∧w∈y∧w⊆z↔w∈y∧x∈w∧w⊆z
9 7 8 bitri ⊢x∈w∧w∈y∩𝒫z↔w∈y∧x∈w∧w⊆z
10 9 exbii ⊢∃wx∈w∧w∈y∩𝒫z↔∃ww∈y∧x∈w∧w⊆z
11 eluni ⊢x∈⋃y∩𝒫z↔∃wx∈w∧w∈y∩𝒫z
12 df-rex ⊢∃w∈yx∈w∧w⊆z↔∃ww∈y∧x∈w∧w⊆z
13 10 11 12 3bitr4i ⊢x∈⋃y∩𝒫z↔∃w∈yx∈w∧w⊆z
14 13 imbi2i ⊢x∈z→x∈⋃y∩𝒫z↔x∈z→∃w∈yx∈w∧w⊆z
15 14 ralbii ⊢∀z∈Jx∈z→x∈⋃y∩𝒫z↔∀z∈Jx∈z→∃w∈yx∈w∧w⊆z
16 15 anbi2i ⊢y≼ω∧∀z∈Jx∈z→x∈⋃y∩𝒫z↔y≼ω∧∀z∈Jx∈z→∃w∈yx∈w∧w⊆z
17 16 rexbii ⊢∃y∈𝒫Jy≼ω∧∀z∈Jx∈z→x∈⋃y∩𝒫z↔∃y∈𝒫Jy≼ω∧∀z∈Jx∈z→∃w∈yx∈w∧w⊆z
18 17 ralbii ⊢∀x∈X∃y∈𝒫Jy≼ω∧∀z∈Jx∈z→x∈⋃y∩𝒫z↔∀x∈X∃y∈𝒫Jy≼ω∧∀z∈Jx∈z→∃w∈yx∈w∧w⊆z
19 18 anbi2i ⊢J∈Top∧∀x∈X∃y∈𝒫Jy≼ω∧∀z∈Jx∈z→x∈⋃y∩𝒫z↔J∈Top∧∀x∈X∃y∈𝒫Jy≼ω∧∀z∈Jx∈z→∃w∈yx∈w∧w⊆z
20 2 19 bitri ⊢J∈1st𝜔↔J∈Top∧∀x∈X∃y∈𝒫Jy≼ω∧∀z∈Jx∈z→∃w∈yx∈w∧w⊆z