This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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