Metamath Proof Explorer


Definition df-locfin

Description: Define "locally finite." (Contributed by Jeff Hankins, 21-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

Ref Expression
Assertion df-locfin LocFin = x Top y | x = y p x n x p n s y | s n Fin

Detailed syntax breakdown

Step Hyp Ref Expression
0 clocfin class LocFin
1 vx setvar x
2 ctop class Top
3 vy setvar y
4 1 cv setvar x
5 4 cuni class x
6 3 cv setvar y
7 6 cuni class y
8 5 7 wceq wff x = y
9 vp setvar p
10 vn setvar n
11 9 cv setvar p
12 10 cv setvar n
13 11 12 wcel wff p n
14 vs setvar s
15 14 cv setvar s
16 15 12 cin class s n
17 c0 class
18 16 17 wne wff s n
19 18 14 6 crab class s y | s n
20 cfn class Fin
21 19 20 wcel wff s y | s n Fin
22 13 21 wa wff p n s y | s n Fin
23 22 10 4 wrex wff n x p n s y | s n Fin
24 23 9 5 wral wff p x n x p n s y | s n Fin
25 8 24 wa wff x = y p x n x p n s y | s n Fin
26 25 3 cab class y | x = y p x n x p n s y | s n Fin
27 1 2 26 cmpt class x Top y | x = y p x n x p n s y | s n Fin
28 0 27 wceq wff LocFin = x Top y | x = y p x n x p n s y | s n Fin