Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-locfin Unicode version

Definition df-locfin 26266
Description: Define "locally finite." (Contributed by Jeff Hankins, 21-Jan-2010.)
Assertion
Ref Expression
df-locfin  |-  LocFin  =  ( x  e.  Top  |->  { y  |  ( U. x  =  U. y  /\  A. p  e.  U. x E. n  e.  x  ( p  e.  n  /\  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin ) ) } )
Distinct variable group:    n, p, s, x, y

Detailed syntax breakdown of Definition df-locfin
StepHypRef Expression
1 clocfin 26262 . 2  class  LocFin
2 vx . . 3  set  x
3 ctop 16631 . . 3  class  Top
42cv 1622 . . . . . . 7  class  x
54cuni 3827 . . . . . 6  class  U. x
6 vy . . . . . . . 8  set  y
76cv 1622 . . . . . . 7  class  y
87cuni 3827 . . . . . 6  class  U. y
95, 8wceq 1623 . . . . 5  wff  U. x  =  U. y
10 vp . . . . . . . . 9  set  p
11 vn . . . . . . . . 9  set  n
1210, 11wel 1685 . . . . . . . 8  wff  p  e.  n
13 vs . . . . . . . . . . . . 13  set  s
1413cv 1622 . . . . . . . . . . . 12  class  s
1511cv 1622 . . . . . . . . . . . 12  class  n
1614, 15cin 3151 . . . . . . . . . . 11  class  ( s  i^i  n )
17 c0 3455 . . . . . . . . . . 11  class  (/)
1816, 17wne 2446 . . . . . . . . . 10  wff  ( s  i^i  n )  =/=  (/)
1918, 13, 7crab 2547 . . . . . . . . 9  class  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }
20 cfn 6863 . . . . . . . . 9  class  Fin
2119, 20wcel 1684 . . . . . . . 8  wff  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin
2212, 21wa 358 . . . . . . 7  wff  ( p  e.  n  /\  {
s  e.  y  |  ( s  i^i  n
)  =/=  (/) }  e.  Fin )
2322, 11, 4wrex 2544 . . . . . 6  wff  E. n  e.  x  ( p  e.  n  /\  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin )
2423, 10, 5wral 2543 . . . . 5  wff  A. p  e.  U. x E. n  e.  x  ( p  e.  n  /\  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin )
259, 24wa 358 . . . 4  wff  ( U. x  =  U. y  /\  A. p  e.  U. x E. n  e.  x  ( p  e.  n  /\  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin ) )
2625, 6cab 2269 . . 3  class  { y  |  ( U. x  =  U. y  /\  A. p  e.  U. x E. n  e.  x  ( p  e.  n  /\  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin ) ) }
272, 3, 26cmpt 4077 . 2  class  ( x  e.  Top  |->  { y  |  ( U. x  =  U. y  /\  A. p  e.  U. x E. n  e.  x  ( p  e.  n  /\  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin ) ) } )
281, 27wceq 1623 1  wff  LocFin  =  ( x  e.  Top  |->  { y  |  ( U. x  =  U. y  /\  A. p  e.  U. x E. n  e.  x  ( p  e.  n  /\  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin ) ) } )
Colors of variables: wff set class
This definition is referenced by:  islocfin  26296
  Copyright terms: Public domain W3C validator