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 \in Top ⟼ \{y \| (⋃ x = ⋃ y \land \forall p \in ⋃ x \exists n \in x (p \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\})$

Step	Hyp	Ref	Expression
0		clocfin	$class LocFin$
1		vx	$setvar x$
2		ctop	$class Top$
3		vy	$setvar y$
4	1	cv	$setvar x$
5	4	cuni	$class ⋃ x$
6	3	cv	$setvar y$
7	6	cuni	$class ⋃ y$
8	5 7	wceq	$wff ⋃ x = ⋃ y$
9		vp	$setvar p$
10		vn	$setvar n$
11	9	cv	$setvar p$
12	10	cv	$setvar n$
13	11 12	wcel	$wff p \in n$
14		vs	$setvar s$
15	14	cv	$setvar s$
16	15 12	cin	$class (s \cap n)$
17		c0	$class \emptyset$
18	16 17	wne	$wff s \cap n \neq \emptyset$
19	18 14 6	crab	$class \{s \in y \| s \cap n \neq \emptyset\}$
20		cfn	$class Fin$
21	19 20	wcel	$wff \{s \in y \| s \cap n \neq \emptyset\} \in Fin$
22	13 21	wa	$wff (p \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin)$
23	22 10 4	wrex	$wff \exists n \in x (p \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin)$
24	23 9 5	wral	$wff \forall p \in ⋃ x \exists n \in x (p \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin)$
25	8 24	wa	$wff (⋃ x = ⋃ y \land \forall p \in ⋃ x \exists n \in x (p \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))$
26	25 3	cab	$class \{y \| (⋃ x = ⋃ y \land \forall p \in ⋃ x \exists n \in x (p \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\}$
27	1 2 26	cmpt	$class (x \in Top ⟼ \{y \| (⋃ x = ⋃ y \land \forall p \in ⋃ x \exists n \in x (p \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\})$
28	0 27	wceq	$wff LocFin = (x \in Top ⟼ \{y \| (⋃ x = ⋃ y \land \forall p \in ⋃ x \exists n \in x (p \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\})$

Metamath Proof Explorer