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 ∈ 1 st 𝜔 ↔ J ∈ Top ∧ ∀ x ∈ X ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → ∃ w ∈ y x ∈ w ∧ w ⊆ z

Proof

Step Hyp Ref Expression
1 is1stc.1 ⊢ X = ⋃ J
2 1 is1stc ⊢ J ∈ 1 st 𝜔 ↔ J ∈ Top ∧ ∀ x ∈ X ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ 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 ⊢ ∃ w x ∈ w ∧ w ∈ y ∩ 𝒫 z ↔ ∃ w w ∈ y ∧ x ∈ w ∧ w ⊆ z
11 eluni ⊢ x ∈ ⋃ y ∩ 𝒫 z ↔ ∃ w x ∈ w ∧ w ∈ y ∩ 𝒫 z
12 df-rex ⊢ ∃ w ∈ y x ∈ w ∧ w ⊆ z ↔ ∃ w w ∈ y ∧ x ∈ w ∧ w ⊆ z
13 10 11 12 3bitr4i ⊢ x ∈ ⋃ y ∩ 𝒫 z ↔ ∃ w ∈ y x ∈ w ∧ w ⊆ z
14 13 imbi2i ⊢ x ∈ z → x ∈ ⋃ y ∩ 𝒫 z ↔ x ∈ z → ∃ w ∈ y x ∈ w ∧ w ⊆ z
15 14 ralbii ⊢ ∀ z ∈ J x ∈ z → x ∈ ⋃ y ∩ 𝒫 z ↔ ∀ z ∈ J x ∈ z → ∃ w ∈ y x ∈ w ∧ w ⊆ z
16 15 anbi2i ⊢ y ≼ ω ∧ ∀ z ∈ J x ∈ z → x ∈ ⋃ y ∩ 𝒫 z ↔ y ≼ ω ∧ ∀ z ∈ J x ∈ z → ∃ w ∈ y x ∈ w ∧ w ⊆ z
17 16 rexbii ⊢ ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → x ∈ ⋃ y ∩ 𝒫 z ↔ ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → ∃ w ∈ y x ∈ w ∧ w ⊆ z
18 17 ralbii ⊢ ∀ x ∈ X ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → x ∈ ⋃ y ∩ 𝒫 z ↔ ∀ x ∈ X ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → ∃ w ∈ y x ∈ w ∧ w ⊆ z
19 18 anbi2i ⊢ J ∈ Top ∧ ∀ x ∈ X ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → x ∈ ⋃ y ∩ 𝒫 z ↔ J ∈ Top ∧ ∀ x ∈ X ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → ∃ w ∈ y x ∈ w ∧ w ⊆ z
20 2 19 bitri ⊢ J ∈ 1 st 𝜔 ↔ J ∈ Top ∧ ∀ x ∈ X ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → ∃ w ∈ y x ∈ w ∧ w ⊆ z