Definition df-locfin 23505

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

Step	Hyp	Ref	Expression
1		clocfin 23502	. 2 class LocFin
2		vx	. . 3 setvar 𝑥
3		ctop 22889	. . 3 class Top
4	2	cv 1539	. . . . . . 7 class 𝑥
5	4	cuni 4905	. . . . . 6 class ∪ 𝑥
6		vy	. . . . . . . 8 setvar 𝑦
7	6	cv 1539	. . . . . . 7 class 𝑦
8	7	cuni 4905	. . . . . 6 class ∪ 𝑦
9	5, 8	wceq 1540	. . . . 5 wff ∪ 𝑥 = ∪ 𝑦
10		vp	. . . . . . . . 9 setvar 𝑝
11		vn	. . . . . . . . 9 setvar 𝑛
12	10, 11	wel 2109	. . . . . . . 8 wff 𝑝 ∈ 𝑛
13		vs	. . . . . . . . . . . . 13 setvar 𝑠
14	13	cv 1539	. . . . . . . . . . . 12 class 𝑠
15	11	cv 1539	. . . . . . . . . . . 12 class 𝑛
16	14, 15	cin 3949	. . . . . . . . . . 11 class (𝑠 ∩ 𝑛)
17		c0 4332	. . . . . . . . . . 11 class ∅
18	16, 17	wne 2939	. . . . . . . . . 10 wff (𝑠 ∩ 𝑛) ≠ ∅
19	18, 13, 7	crab 3435	. . . . . . . . 9 class {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅}
20		cfn 8981	. . . . . . . . 9 class Fin
21	19, 20	wcel 2108	. . . . . . . 8 wff {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin
22	12, 21	wa 395	. . . . . . 7 wff (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)
23	22, 11, 4	wrex 3069	. . . . . 6 wff ∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)
24	23, 10, 5	wral 3060	. . . . 5 wff ∀𝑝 ∈ ∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)
25	9, 24	wa 395	. . . 4 wff (∪ 𝑥 = ∪ 𝑦 ∧ ∀𝑝 ∈ ∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))
26	25, 6	cab 2713	. . 3 class {𝑦 ∣ (∪ 𝑥 = ∪ 𝑦 ∧ ∀𝑝 ∈ ∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))}
27	2, 3, 26	cmpt 5223	. 2 class (𝑥 ∈ Top ↦ {𝑦 ∣ (∪ 𝑥 = ∪ 𝑦 ∧ ∀𝑝 ∈ ∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))})
28	1, 27	wceq 1540	1 wff LocFin = (𝑥 ∈ Top ↦ {𝑦 ∣ (∪ 𝑥 = ∪ 𝑦 ∧ ∀𝑝 ∈ ∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))})

This definition is referenced by:  islocfin  23515