lfinpfin

Description: A locally finite cover is point-finite. (Contributed by Jeff Hankins, 21-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

		Ref	Expression
	Assertion	lfinpfin	$⊢ A \in LocFin (J) \to A \in PtFin$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2		eqid	$⊢ ⋃ A = ⋃ A$
3	1 2	locfinbas	$⊢ A \in LocFin (J) \to ⋃ J = ⋃ A$
4	3	eleq2d	$⊢ A \in LocFin (J) \to (x \in ⋃ J \leftrightarrow x \in ⋃ A)$
5	4	biimpar	$⊢ (A \in LocFin (J) \land x \in ⋃ A) \to x \in ⋃ J$
6	1	locfinnei	$⊢ (A \in LocFin (J) \land x \in ⋃ J) \to \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)$
7	5 6	syldan	$⊢ (A \in LocFin (J) \land x \in ⋃ A) \to \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)$
8		inelcm	$⊢ (x \in s \land x \in n) \to s \cap n \neq \emptyset$
9	8	expcom	$⊢ x \in n \to (x \in s \to s \cap n \neq \emptyset)$
10	9	ad2antlr	$⊢ (((A \in LocFin (J) \land x \in ⋃ A) \land x \in n) \land s \in A) \to (x \in s \to s \cap n \neq \emptyset)$
11	10	ss2rabdv	$⊢ ((A \in LocFin (J) \land x \in ⋃ A) \land x \in n) \to \{s \in A \| x \in s\} \subseteq \{s \in A \| s \cap n \neq \emptyset\}$
12		ssfi	$⊢ (\{s \in A \| s \cap n \neq \emptyset\} \in Fin \land \{s \in A \| x \in s\} \subseteq \{s \in A \| s \cap n \neq \emptyset\}) \to \{s \in A \| x \in s\} \in Fin$
13	12	expcom	$⊢ \{s \in A \| x \in s\} \subseteq \{s \in A \| s \cap n \neq \emptyset\} \to (\{s \in A \| s \cap n \neq \emptyset\} \in Fin \to \{s \in A \| x \in s\} \in Fin)$
14	11 13	syl	$⊢ ((A \in LocFin (J) \land x \in ⋃ A) \land x \in n) \to (\{s \in A \| s \cap n \neq \emptyset\} \in Fin \to \{s \in A \| x \in s\} \in Fin)$
15	14	expimpd	$⊢ (A \in LocFin (J) \land x \in ⋃ A) \to ((x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin) \to \{s \in A \| x \in s\} \in Fin)$
16	15	rexlimdvw	$⊢ (A \in LocFin (J) \land x \in ⋃ A) \to (\exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin) \to \{s \in A \| x \in s\} \in Fin)$
17	7 16	mpd	$⊢ (A \in LocFin (J) \land x \in ⋃ A) \to \{s \in A \| x \in s\} \in Fin$
18	17	ralrimiva	$⊢ A \in LocFin (J) \to \forall x \in ⋃ A \{s \in A \| x \in s\} \in Fin$
19	2	isptfin	$⊢ A \in LocFin (J) \to (A \in PtFin \leftrightarrow \forall x \in ⋃ A \{s \in A \| x \in s\} \in Fin)$
20	18 19	mpbird	$⊢ A \in LocFin (J) \to A \in PtFin$

Metamath Proof Explorer

Theorem lfinpfin

Proof