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