Definition df-locfin 21310

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

Step	Hyp	Ref	Expression
1		clocfin 21307	. 2 class LocFin
2		vx	. . 3 setvar x
3		ctop 20698	. . 3 class Top
4	2	cv 1482	. . . . . . 7 class x
5	4	cuni 4436	. . . . . 6 class U. x
6		vy	. . . . . . . 8 setvar y
7	6	cv 1482	. . . . . . 7 class y
8	7	cuni 4436	. . . . . 6 class U. y
9	5, 8	wceq 1483	. . . . 5 wff U. x = U. y
10		vp	. . . . . . . . 9 setvar p
11		vn	. . . . . . . . 9 setvar n
12	10, 11	wel 1991	. . . . . . . 8 wff p e. n
13		vs	. . . . . . . . . . . . 13 setvar s
14	13	cv 1482	. . . . . . . . . . . 12 class s
15	11	cv 1482	. . . . . . . . . . . 12 class n
16	14, 15	cin 3573	. . . . . . . . . . 11 class ( s i^i n )
17		c0 3915	. . . . . . . . . . 11 class (/)
18	16, 17	wne 2794	. . . . . . . . . 10 wff ( s i^i n ) =/= (/)
19	18, 13, 7	crab 2916	. . . . . . . . 9 class { s e. y | ( s i^i n ) =/= (/) }
20		cfn 7955	. . . . . . . . 9 class Fin
21	19, 20	wcel 1990	. . . . . . . 8 wff { s e. y | ( s i^i n ) =/= (/) } e. Fin
22	12, 21	wa 384	. . . . . . 7 wff ( p e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin )
23	22, 11, 4	wrex 2913	. . . . . 6 wff E. n e. x ( p e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin )
24	23, 10, 5	wral 2912	. . . . 5 wff A. p e. U. x E. n e. x ( p e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin )
25	9, 24	wa 384	. . . 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 ) )
26	25, 6	cab 2608	. . 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 ) ) }
27	2, 3, 26	cmpt 4729	. 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 ) ) } )
28	1, 27	wceq 1483	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 ) ) } )

This definition is referenced by:  islocfin  21320