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 27206
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 27204 . 2  class TopLnd
2 vx . . . . . . . 8  set  x
32cv 1648 . . . . . . 7  class  x
43cuni 3959 . . . . . 6  class  U. x
5 vy . . . . . . . 8  set  y
65cv 1648 . . . . . . 7  class  y
76cuni 3959 . . . . . 6  class  U. y
84, 7wceq 1649 . . . . 5  wff  U. x  =  U. y
9 vz . . . . . . . . 9  set  z
109cv 1648 . . . . . . . 8  class  z
11 com 4787 . . . . . . . 8  class  om
12 cdom 7045 . . . . . . . 8  class  ~<_
1310, 11, 12wbr 4155 . . . . . . 7  wff  z  ~<_  om
1410cuni 3959 . . . . . . . 8  class  U. z
154, 14wceq 1649 . . . . . . 7  wff  U. x  =  U. z
1613, 15wa 359 . . . . . 6  wff  ( z  ~<_  om  /\  U. x  =  U. z )
173cpw 3744 . . . . . 6  class  ~P x
1816, 9, 17wrex 2652 . . . . 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 2651 . . 3  wff  A. y  e.  ~P  x ( U. x  =  U. y  ->  E. z  e.  ~P  x ( z  ~<_  om 
/\  U. x  =  U. z ) )
21 ctop 16883 . . 3  class  Top
2220, 2, 21crab 2655 . 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 1649 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