MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-locfin Structured version   Unicode version

Definition df-locfin 20459
Description: Define "locally finite." (Contributed by Jeff Hankins, 21-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.)
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 20456 . 2  class  LocFin
2 vx . . 3  setvar  x
3 ctop 19854 . . 3  class  Top
42cv 1436 . . . . . . 7  class  x
54cuni 4213 . . . . . 6  class  U. x
6 vy . . . . . . . 8  setvar  y
76cv 1436 . . . . . . 7  class  y
87cuni 4213 . . . . . 6  class  U. y
95, 8wceq 1437 . . . . 5  wff  U. x  =  U. y
10 vp . . . . . . . . 9  setvar  p
11 vn . . . . . . . . 9  setvar  n
1210, 11wel 1868 . . . . . . . 8  wff  p  e.  n
13 vs . . . . . . . . . . . . 13  setvar  s
1413cv 1436 . . . . . . . . . . . 12  class  s
1511cv 1436 . . . . . . . . . . . 12  class  n
1614, 15cin 3432 . . . . . . . . . . 11  class  ( s  i^i  n )
17 c0 3758 . . . . . . . . . . 11  class  (/)
1816, 17wne 2616 . . . . . . . . . 10  wff  ( s  i^i  n )  =/=  (/)
1918, 13, 7crab 2777 . . . . . . . . 9  class  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }
20 cfn 7568 . . . . . . . . 9  class  Fin
2119, 20wcel 1867 . . . . . . . 8  wff  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin
2212, 21wa 370 . . . . . . 7  wff  ( p  e.  n  /\  {
s  e.  y  |  ( s  i^i  n
)  =/=  (/) }  e.  Fin )
2322, 11, 4wrex 2774 . . . . . 6  wff  E. n  e.  x  ( p  e.  n  /\  { s  e.  y  |  ( s  i^i  n )  =/=  (/) }  e.  Fin )
2423, 10, 5wral 2773 . . . . 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 370 . . . 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 2405 . . 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 4475 . 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 1437 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 setvar class
This definition is referenced by:  islocfin  20469
  Copyright terms: Public domain W3C validator