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

Definition df-locfin 26346
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 26342 . 2  class  LocFin
2 vx . . 3  set  x
3 ctop 16958 . . 3  class  Top
42cv 1651 . . . . . . 7  class  x
54cuni 4015 . . . . . 6  class  U. x
6 vy . . . . . . . 8  set  y
76cv 1651 . . . . . . 7  class  y
87cuni 4015 . . . . . 6  class  U. y
95, 8wceq 1652 . . . . 5  wff  U. x  =  U. y
10 vp . . . . . . . . 9  set  p
11 vn . . . . . . . . 9  set  n
1210, 11wel 1726 . . . . . . . 8  wff  p  e.  n
13 vs . . . . . . . . . . . . 13  set  s
1413cv 1651 . . . . . . . . . . . 12  class  s
1511cv 1651 . . . . . . . . . . . 12  class  n
1614, 15cin 3319 . . . . . . . . . . 11  class  ( s  i^i  n )
17 c0 3628 . . . . . . . . . . 11  class  (/)
1816, 17wne 2599 . . . . . . . . . 10  wff  ( s  i^i  n )  =/=  (/)
1918, 13, 7crab 2709 . . . . . . . . 9  class  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }
20 cfn 7109 . . . . . . . . 9  class  Fin
2119, 20wcel 1725 . . . . . . . 8  wff  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin
2212, 21wa 359 . . . . . . 7  wff  ( p  e.  n  /\  {
s  e.  y  |  ( s  i^i  n
)  =/=  (/) }  e.  Fin )
2322, 11, 4wrex 2706 . . . . . 6  wff  E. n  e.  x  ( p  e.  n  /\  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin )
2423, 10, 5wral 2705 . . . . 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 359 . . . 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 2422 . . 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 4266 . 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 1652 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  26376
  Copyright terms: Public domain W3C validator