MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-locfin Structured version   Visualization version   GIF version

Definition df-locfin 21120
Description: Define "locally finite." (Contributed by Jeff Hankins, 21-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.)
Assertion
Ref Expression
df-locfin LocFin = (𝑥 ∈ Top ↦ {𝑦 ∣ ( 𝑥 = 𝑦 ∧ ∀𝑝 𝑥𝑛𝑥 (𝑝𝑛 ∧ {𝑠𝑦 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin))})
Distinct variable group:   𝑛,𝑝,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-locfin
StepHypRef Expression
1 clocfin 21117 . 2 class LocFin
2 vx . . 3 setvar 𝑥
3 ctop 20517 . . 3 class Top
42cv 1474 . . . . . . 7 class 𝑥
54cuni 4372 . . . . . 6 class 𝑥
6 vy . . . . . . . 8 setvar 𝑦
76cv 1474 . . . . . . 7 class 𝑦
87cuni 4372 . . . . . 6 class 𝑦
95, 8wceq 1475 . . . . 5 wff 𝑥 = 𝑦
10 vp . . . . . . . . 9 setvar 𝑝
11 vn . . . . . . . . 9 setvar 𝑛
1210, 11wel 1978 . . . . . . . 8 wff 𝑝𝑛
13 vs . . . . . . . . . . . . 13 setvar 𝑠
1413cv 1474 . . . . . . . . . . . 12 class 𝑠
1511cv 1474 . . . . . . . . . . . 12 class 𝑛
1614, 15cin 3539 . . . . . . . . . . 11 class (𝑠𝑛)
17 c0 3874 . . . . . . . . . . 11 class
1816, 17wne 2780 . . . . . . . . . 10 wff (𝑠𝑛) ≠ ∅
1918, 13, 7crab 2900 . . . . . . . . 9 class {𝑠𝑦 ∣ (𝑠𝑛) ≠ ∅}
20 cfn 7841 . . . . . . . . 9 class Fin
2119, 20wcel 1977 . . . . . . . 8 wff {𝑠𝑦 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin
2212, 21wa 383 . . . . . . 7 wff (𝑝𝑛 ∧ {𝑠𝑦 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin)
2322, 11, 4wrex 2897 . . . . . 6 wff 𝑛𝑥 (𝑝𝑛 ∧ {𝑠𝑦 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin)
2423, 10, 5wral 2896 . . . . 5 wff 𝑝 𝑥𝑛𝑥 (𝑝𝑛 ∧ {𝑠𝑦 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin)
259, 24wa 383 . . . 4 wff ( 𝑥 = 𝑦 ∧ ∀𝑝 𝑥𝑛𝑥 (𝑝𝑛 ∧ {𝑠𝑦 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin))
2625, 6cab 2596 . . 3 class {𝑦 ∣ ( 𝑥 = 𝑦 ∧ ∀𝑝 𝑥𝑛𝑥 (𝑝𝑛 ∧ {𝑠𝑦 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin))}
272, 3, 26cmpt 4643 . 2 class (𝑥 ∈ Top ↦ {𝑦 ∣ ( 𝑥 = 𝑦 ∧ ∀𝑝 𝑥𝑛𝑥 (𝑝𝑛 ∧ {𝑠𝑦 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin))})
281, 27wceq 1475 1 wff LocFin = (𝑥 ∈ Top ↦ {𝑦 ∣ ( 𝑥 = 𝑦 ∧ ∀𝑝 𝑥𝑛𝑥 (𝑝𝑛 ∧ {𝑠𝑦 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin))})
Colors of variables: wff setvar class
This definition is referenced by:  islocfin  21130
  Copyright terms: Public domain W3C validator