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 = ( 𝑥 ∈ Top ↦ { 𝑦 ∣ ( 𝑥 = 𝑦 ∧ ∀ 𝑝 𝑥𝑛𝑥 ( 𝑝𝑛 ∧ { 𝑠𝑦 ∣ ( 𝑠𝑛 ) ≠ ∅ } ∈ Fin ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clocfin LocFin
1 vx 𝑥
2 ctop Top
3 vy 𝑦
4 1 cv 𝑥
5 4 cuni 𝑥
6 3 cv 𝑦
7 6 cuni 𝑦
8 5 7 wceq 𝑥 = 𝑦
9 vp 𝑝
10 vn 𝑛
11 9 cv 𝑝
12 10 cv 𝑛
13 11 12 wcel 𝑝𝑛
14 vs 𝑠
15 14 cv 𝑠
16 15 12 cin ( 𝑠𝑛 )
17 c0
18 16 17 wne ( 𝑠𝑛 ) ≠ ∅
19 18 14 6 crab { 𝑠𝑦 ∣ ( 𝑠𝑛 ) ≠ ∅ }
20 cfn Fin
21 19 20 wcel { 𝑠𝑦 ∣ ( 𝑠𝑛 ) ≠ ∅ } ∈ Fin
22 13 21 wa ( 𝑝𝑛 ∧ { 𝑠𝑦 ∣ ( 𝑠𝑛 ) ≠ ∅ } ∈ Fin )
23 22 10 4 wrex 𝑛𝑥 ( 𝑝𝑛 ∧ { 𝑠𝑦 ∣ ( 𝑠𝑛 ) ≠ ∅ } ∈ Fin )
24 23 9 5 wral 𝑝 𝑥𝑛𝑥 ( 𝑝𝑛 ∧ { 𝑠𝑦 ∣ ( 𝑠𝑛 ) ≠ ∅ } ∈ Fin )
25 8 24 wa ( 𝑥 = 𝑦 ∧ ∀ 𝑝 𝑥𝑛𝑥 ( 𝑝𝑛 ∧ { 𝑠𝑦 ∣ ( 𝑠𝑛 ) ≠ ∅ } ∈ Fin ) )
26 25 3 cab { 𝑦 ∣ ( 𝑥 = 𝑦 ∧ ∀ 𝑝 𝑥𝑛𝑥 ( 𝑝𝑛 ∧ { 𝑠𝑦 ∣ ( 𝑠𝑛 ) ≠ ∅ } ∈ Fin ) ) }
27 1 2 26 cmpt ( 𝑥 ∈ Top ↦ { 𝑦 ∣ ( 𝑥 = 𝑦 ∧ ∀ 𝑝 𝑥𝑛𝑥 ( 𝑝𝑛 ∧ { 𝑠𝑦 ∣ ( 𝑠𝑛 ) ≠ ∅ } ∈ Fin ) ) } )
28 0 27 wceq LocFin = ( 𝑥 ∈ Top ↦ { 𝑦 ∣ ( 𝑥 = 𝑦 ∧ ∀ 𝑝 𝑥𝑛𝑥 ( 𝑝𝑛 ∧ { 𝑠𝑦 ∣ ( 𝑠𝑛 ) ≠ ∅ } ∈ Fin ) ) } )