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
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-locfin
StepHypRef Expression
1 clocfin 20456 . 2
2 vx . . 3
3 ctop 19854 . . 3
42cv 1436 . . . . . . 7
54cuni 4213 . . . . . 6
6 vy . . . . . . . 8
76cv 1436 . . . . . . 7
87cuni 4213 . . . . . 6
95, 8wceq 1437 . . . . 5
10 vp . . . . . . . . 9
11 vn . . . . . . . . 9
1210, 11wel 1868 . . . . . . . 8
13 vs . . . . . . . . . . . . 13
1413cv 1436 . . . . . . . . . . . 12
1511cv 1436 . . . . . . . . . . . 12
1614, 15cin 3432 . . . . . . . . . . 11
17 c0 3758 . . . . . . . . . . 11
1816, 17wne 2616 . . . . . . . . . 10
1918, 13, 7crab 2777 . . . . . . . . 9
20 cfn 7568 . . . . . . . . 9
2119, 20wcel 1867 . . . . . . . 8
2212, 21wa 370 . . . . . . 7
2322, 11, 4wrex 2774 . . . . . 6
2423, 10, 5wral 2773 . . . . 5
259, 24wa 370 . . . 4
2625, 6cab 2405 . . 3
272, 3, 26cmpt 4475 . 2
281, 27wceq 1437 1
 Colors of variables: wff setvar class This definition is referenced by:  islocfin  20469
 Copyright terms: Public domain W3C validator