Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-toplnd Unicode version

Definition df-toplnd 27535
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
StepHypRef Expression
1 ctoplnd 27533 . 2  class TopLnd
2 vx . . . . . . . 8  set  x
32cv 1622 . . . . . . 7  class  x
43cuni 3827 . . . . . 6  class  U. x
5 vy . . . . . . . 8  set  y
65cv 1622 . . . . . . 7  class  y
76cuni 3827 . . . . . 6  class  U. y
84, 7wceq 1623 . . . . 5  wff  U. x  =  U. y
9 vz . . . . . . . . 9  set  z
109cv 1622 . . . . . . . 8  class  z
11 com 4656 . . . . . . . 8  class  om
12 cdom 6861 . . . . . . . 8  class  ~<_
1310, 11, 12wbr 4023 . . . . . . 7  wff  z  ~<_  om
1410cuni 3827 . . . . . . . 8  class  U. z
154, 14wceq 1623 . . . . . . 7  wff  U. x  =  U. z
1613, 15wa 358 . . . . . 6  wff  ( z  ~<_  om  /\  U. x  =  U. z )
173cpw 3625 . . . . . 6  class  ~P x
1816, 9, 17wrex 2544 . . . . 5  wff  E. z  e.  ~P  x ( z  ~<_  om  /\  U. x  =  U. z )
198, 18wi 4 . . . 4  wff  ( U. x  =  U. y  ->  E. z  e.  ~P  x ( z  ~<_  om 
/\  U. x  =  U. z ) )
2019, 5, 17wral 2543 . . 3  wff  A. y  e.  ~P  x ( U. x  =  U. y  ->  E. z  e.  ~P  x ( z  ~<_  om 
/\  U. x  =  U. z ) )
21 ctop 16631 . . 3  class  Top
2220, 2, 21crab 2547 . 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 ) ) }
231, 22wceq 1623 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 ) ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator