This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
Assertion is1stc2 ( 𝐽 ∈ 1stω ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 is1stc.1 ⊢ 𝑋 = ∪ 𝐽
2 1 is1stc ⊢ ( 𝐽 ∈ 1stω ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ) )
3 elin ⊢ ( 𝑤 ∈ ( 𝑦 ∩ 𝒫 𝑧 ) ↔ ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝒫 𝑧 ) )
4 velpw ⊢ ( 𝑤 ∈ 𝒫 𝑧 ↔ 𝑤 ⊆ 𝑧 )
5 4 anbi2i ⊢ ( ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝒫 𝑧 ) ↔ ( 𝑤 ∈ 𝑦 ∧ 𝑤 ⊆ 𝑧 ) )
6 3 5 bitri ⊢ ( 𝑤 ∈ ( 𝑦 ∩ 𝒫 𝑧 ) ↔ ( 𝑤 ∈ 𝑦 ∧ 𝑤 ⊆ 𝑧 ) )
7 6 anbi2i ⊢ ( ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑦 ∩ 𝒫 𝑧 ) ) ↔ ( 𝑥 ∈ 𝑤 ∧ ( 𝑤 ∈ 𝑦 ∧ 𝑤 ⊆ 𝑧 ) ) )
8 an12 ⊢ ( ( 𝑥 ∈ 𝑤 ∧ ( 𝑤 ∈ 𝑦 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ( 𝑤 ∈ 𝑦 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
9 7 8 bitri ⊢ ( ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑦 ∩ 𝒫 𝑧 ) ) ↔ ( 𝑤 ∈ 𝑦 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
10 9 exbii ⊢ ( ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑦 ∩ 𝒫 𝑧 ) ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
11 eluni ⊢ ( 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ↔ ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑦 ∩ 𝒫 𝑧 ) ) )
12 df-rex ⊢ ( ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
13 10 11 12 3bitr4i ⊢ ( 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ↔ ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) )
14 13 imbi2i ⊢ ( ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ↔ ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
15 14 ralbii ⊢ ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
16 15 anbi2i ⊢ ( ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ↔ ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
17 16 rexbii ⊢ ( ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ↔ ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
18 17 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
19 18 anbi2i ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ) ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
20 2 19 bitri ⊢ ( 𝐽 ∈ 1stω ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )