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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctoplnd	|- TopLnd
1		vx	|- x
2		ctop	|- Top
3		vy	|- y
4	1	cv	|- x
5	4	cpw	|- ~P x
6	4	cuni	|- U. x
7	3	cv	|- y
8	7	cuni	|- U. y
9	6 8	wceq	|- U. x = U. y
10		vz	|- z
11	10	cv	|- z
12		cdom	|- ~<_
13		com	|- _om
14	11 13 12	wbr	|- z ~<_ _om
15	11	cuni	|- U. z
16	6 15	wceq	|- U. x = U. z
17	14 16	wa	|- ( z ~<_ _om /\ U. x = U. z )
18	17 10 5	wrex	|- E. z e. ~P x ( z ~<_ _om /\ U. x = U. z )
19	9 18	wi	|- ( U. x = U. y -> E. z e. ~P x ( z ~<_ _om /\ U. x = U. z ) )
20	19 3 5	wral	|- A. y e. ~P x ( U. x = U. y -> E. z e. ~P x ( z ~<_ _om /\ U. x = U. z ) )
21	20 1 2	crab	|- { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ~P x ( z ~<_ _om /\ U. x = U. z ) ) }
22	0 21	wceq	|- TopLnd = { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ~P x ( z ~<_ _om /\ U. x = U. z ) ) }