Definition df-toplnd

Description: A topology isLindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015)

	Ref	Expression
Assertion	df-toplnd	⊢ TopLnd = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( ∪ 𝑥 = ∪ 𝑦 → ∃ 𝑧 ∈ 𝒫 𝑥 ( 𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧 ) ) }

Detailed syntax breakdown

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