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	$$⊢\mathrm{TopLnd}=\left\{x\in \mathrm{Top}|\forall y\in 𝒫x\left(\bigcup x=\bigcup y\to \exists z\in 𝒫x\left(z\preccurlyeq \mathrm{\omega }\wedge \bigcup x=\bigcup z\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctoplnd	$$class\mathrm{TopLnd}$$
1		vx	$$setvarx$$
2		ctop	$$class\mathrm{Top}$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5	4	cpw	$$class𝒫x$$
6	4	cuni	$$class\bigcup x$$
7	3	cv	$$setvary$$
8	7	cuni	$$class\bigcup y$$
9	6 8	wceq	$$wff\bigcup x=\bigcup y$$
10		vz	$$setvarz$$
11	10	cv	$$setvarz$$
12		cdom	$$class\preccurlyeq$$
13		com	$$class\mathrm{\omega }$$
14	11 13 12	wbr	$$wffz\preccurlyeq \mathrm{\omega }$$
15	11	cuni	$$class\bigcup z$$
16	6 15	wceq	$$wff\bigcup x=\bigcup z$$
17	14 16	wa	$$wff\left(z\preccurlyeq \mathrm{\omega }\wedge \bigcup x=\bigcup z\right)$$
18	17 10 5	wrex	$$wff\exists z\in 𝒫x\left(z\preccurlyeq \mathrm{\omega }\wedge \bigcup x=\bigcup z\right)$$
19	9 18	wi	$$wff\left(\bigcup x=\bigcup y\to \exists z\in 𝒫x\left(z\preccurlyeq \mathrm{\omega }\wedge \bigcup x=\bigcup z\right)\right)$$
20	19 3 5	wral	$$wff\forall y\in 𝒫x\left(\bigcup x=\bigcup y\to \exists z\in 𝒫x\left(z\preccurlyeq \mathrm{\omega }\wedge \bigcup x=\bigcup z\right)\right)$$
21	20 1 2	crab	$$class\left\{x\in \mathrm{Top}|\forall y\in 𝒫x\left(\bigcup x=\bigcup y\to \exists z\in 𝒫x\left(z\preccurlyeq \mathrm{\omega }\wedge \bigcup x=\bigcup z\right)\right)\right\}$$
22	0 21	wceq	$$wff\mathrm{TopLnd}=\left\{x\in \mathrm{Top}|\forall y\in 𝒫x\left(\bigcup x=\bigcup y\to \exists z\in 𝒫x\left(z\preccurlyeq \mathrm{\omega }\wedge \bigcup x=\bigcup z\right)\right)\right\}$$