This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem finptfin

Description: A finite cover is a point-finite cover. (Contributed by Jeff Hankins, 21-Jan-2010)

		Ref	Expression
	Assertion	finptfin	$⊢ A \in Fin \to A \in PtFin$

Step	Hyp	Ref	Expression
1		rabfi	$⊢ A \in Fin \to \{y \in A \| x \in y\} \in Fin$
2	1	ralrimivw	$⊢ A \in Fin \to \forall x \in ⋃ A \{y \in A \| x \in y\} \in Fin$
3		eqid	$⊢ ⋃ A = ⋃ A$
4	3	isptfin	$⊢ A \in Fin \to (A \in PtFin \leftrightarrow \forall x \in ⋃ A \{y \in A \| x \in y\} \in Fin)$
5	2 4	mpbird	$⊢ A \in Fin \to A \in PtFin$