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

Metamath Proof Explorer

Definition df-1stc

Description: Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009)

Ref Expression
Assertion df-1stc 1stω = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 c1stc ⊢ 1stω
1 vj ⊢ 𝑗
2 ctop ⊢ Top
3 vx ⊢ 𝑥
4 1 cv ⊢ 𝑗
5 4 cuni ⊢ ∪ 𝑗
6 vy ⊢ 𝑦
7 4 cpw ⊢ 𝒫 𝑗
8 6 cv ⊢ 𝑦
9 cdom ⊢ ≼
10 com ⊢ ω
11 8 10 9 wbr ⊢ 𝑦 ≼ ω
12 vz ⊢ 𝑧
13 3 cv ⊢ 𝑥
14 12 cv ⊢ 𝑧
15 13 14 wcel ⊢ 𝑥 ∈ 𝑧
16 14 cpw ⊢ 𝒫 𝑧
17 8 16 cin ⊢ ( 𝑦 ∩ 𝒫 𝑧 )
18 17 cuni ⊢ ∪ ( 𝑦 ∩ 𝒫 𝑧 )
19 13 18 wcel ⊢ 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 )
20 15 19 wi ⊢ ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) )
21 20 12 4 wral ⊢ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) )
22 11 21 wa ⊢ ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) )
23 22 6 7 wrex ⊢ ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) )
24 23 3 5 wral ⊢ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) )
25 24 1 2 crab ⊢ { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) }
26 0 25 wceq ⊢ 1stω = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) }