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

Definition df-locfin 26369
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 26365 . 2  class  LocFin
2 vx . . 3  set  x
3 ctop 16647 . . 3  class  Top
42cv 1631 . . . . . . 7  class  x
54cuni 3843 . . . . . 6  class  U. x
6 vy . . . . . . . 8  set  y
76cv 1631 . . . . . . 7  class  y
87cuni 3843 . . . . . 6  class  U. y
95, 8wceq 1632 . . . . 5  wff  U. x  =  U. y
10 vp . . . . . . . . 9  set  p
11 vn . . . . . . . . 9  set  n
1210, 11wel 1697 . . . . . . . 8  wff  p  e.  n
13 vs . . . . . . . . . . . . 13  set  s
1413cv 1631 . . . . . . . . . . . 12  class  s
1511cv 1631 . . . . . . . . . . . 12  class  n
1614, 15cin 3164 . . . . . . . . . . 11  class  ( s  i^i  n )
17 c0 3468 . . . . . . . . . . 11  class  (/)
1816, 17wne 2459 . . . . . . . . . 10  wff  ( s  i^i  n )  =/=  (/)
1918, 13, 7crab 2560 . . . . . . . . 9  class  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }
20 cfn 6879 . . . . . . . . 9  class  Fin
2119, 20wcel 1696 . . . . . . . 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 2557 . . . . . 6  wff  E. n  e.  x  ( p  e.  n  /\  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin )
2423, 10, 5wral 2556 . . . . 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 2282 . . 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 4093 . 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 1632 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  26399
  Copyright terms: Public domain W3C validator