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 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 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clocfin	|- LocFin
1		vx	|- x
2		ctop	|- Top
3		vy	|- y
4	1	cv	|- x
5	4	cuni	|- U. x
6	3	cv	|- y
7	6	cuni	|- U. y
8	5 7	wceq	|- U. x = U. y
9		vp	|- p
10		vn	|- n
11	9	cv	|- p
12	10	cv	|- n
13	11 12	wcel	|- p e. n
14		vs	|- s
15	14	cv	|- s
16	15 12	cin	|- ( s i^i n )
17		c0	|- (/)
18	16 17	wne	|- ( s i^i n ) =/= (/)
19	18 14 6	crab	|- { s e. y | ( s i^i n ) =/= (/) }
20		cfn	|- Fin
21	19 20	wcel	|- { s e. y | ( s i^i n ) =/= (/) } e. Fin
22	13 21	wa	|- ( p e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin )
23	22 10 4	wrex	|- E. n e. x ( p e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin )
24	23 9 5	wral	|- A. p e. U. x E. n e. x ( p e. n /\ { s e. y | ( s i^i n ) =/= (/) } e. Fin )
25	8 24	wa	|- ( 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 3	cab	|- { 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	1 2 26	cmpt	|- ( 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	0 27	wceq	|- 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 ) ) } )