Definition df-toplnd 44305

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

Assertion

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

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-toplnd

Step	Hyp	Ref	Expression
1		ctoplnd 44303	. 2 class TopLnd
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1568	. . . . . . 7 class 𝑥
4	3	cuni 4866	. . . . . 6 class ∪ 𝑥
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1568	. . . . . . 7 class 𝑦
7	6	cuni 4866	. . . . . 6 class ∪ 𝑦
8	4, 7	wceq 1569	. . . . 5 wff ∪ 𝑥 = ∪ 𝑦
9		vz	. . . . . . . . 9 setvar 𝑧
10	9	cv 1568	. . . . . . . 8 class 𝑧
11		com 7878	. . . . . . . 8 class ω
12		cdom 8975	. . . . . . . 8 class ≼
13	10, 11, 12	wbr 5102	. . . . . . 7 wff 𝑧 ≼ ω
14	10	cuni 4866	. . . . . . . 8 class ∪ 𝑧
15	4, 14	wceq 1569	. . . . . . 7 wff ∪ 𝑥 = ∪ 𝑧
16	13, 15	wa 401	. . . . . 6 wff (𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧)
17	3	cpw 4556	. . . . . 6 class 𝒫 𝑥
18	16, 9, 17	wrex 3086	. . . . 5 wff ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧)
19	8, 18	wi 4	. . . 4 wff (∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧))
20	19, 5, 17	wral 3076	. . 3 wff ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧))
21		ctop 23217	. . 3 class Top
22	20, 2, 21	crab 3412	. 2 class {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧))}
23	1, 22	wceq 1569	1 wff TopLnd = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧))}

This definition is used by: (None)