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 ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) }