Theorem finptfin

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

	Ref	Expression
Assertion	finptfin	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ PtFin )

Proof

Step	Hyp	Ref	Expression
1		rabfi	⊢ ( 𝐴 ∈ Fin → { 𝑦 ∈ 𝐴 ∣ 𝑥 ∈ 𝑦 } ∈ Fin )
2	1	ralrimivw	⊢ ( 𝐴 ∈ Fin → ∀ 𝑥 ∈ ∪ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑥 ∈ 𝑦 } ∈ Fin )
3		eqid	⊢ ∪ 𝐴 = ∪ 𝐴
4	3	isptfin	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∈ PtFin ↔ ∀ 𝑥 ∈ ∪ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑥 ∈ 𝑦 } ∈ Fin ) )
5	2 4	mpbird	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ PtFin )