Definition df-toplnd 37794

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 = { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ~P x ( z ~<_ om /\ U. x = U. z ) ) }

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-toplnd

Step	Hyp	Ref	Expression
1		ctoplnd 37792	. 2 class TopLnd
2		vx	. . . . . . . 8 setvar x
3	2	cv 1482	. . . . . . 7 class x
4	3	cuni 4436	. . . . . 6 class U. x
5		vy	. . . . . . . 8 setvar y
6	5	cv 1482	. . . . . . 7 class y
7	6	cuni 4436	. . . . . 6 class U. y
8	4, 7	wceq 1483	. . . . 5 wff U. x = U. y
9		vz	. . . . . . . . 9 setvar z
10	9	cv 1482	. . . . . . . 8 class z
11		com 7065	. . . . . . . 8 class om
12		cdom 7953	. . . . . . . 8 class ~<_
13	10, 11, 12	wbr 4653	. . . . . . 7 wff z ~<_ om
14	10	cuni 4436	. . . . . . . 8 class U. z
15	4, 14	wceq 1483	. . . . . . 7 wff U. x = U. z
16	13, 15	wa 384	. . . . . 6 wff ( z ~<_ om /\ U. x = U. z )
17	3	cpw 4158	. . . . . 6 class ~P x
18	16, 9, 17	wrex 2913	. . . . 5 wff E. z e. ~P x ( z ~<_ om /\ U. x = U. z )
19	8, 18	wi 4	. . . 4 wff ( U. x = U. y -> E. z e. ~P x ( z ~<_ om /\ U. x = U. z ) )
20	19, 5, 17	wral 2912	. . 3 wff A. y e. ~P x ( U. x = U. y -> E. z e. ~P x ( z ~<_ om /\ U. x = U. z ) )
21		ctop 20698	. . 3 class Top
22	20, 2, 21	crab 2916	. 2 class { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ~P x ( z ~<_ om /\ U. x = U. z ) ) }
23	1, 22	wceq 1483	1 wff TopLnd = { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ~P x ( z ~<_ om /\ U. x = U. z ) ) }

This definition is referenced by: (None)