Theorem ptfinfin

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

	Ref	Expression
Hypothesis	ptfinfin.1	⊢ 𝑋 = ∪ 𝐴
Assertion	ptfinfin	⊢ ( ( 𝐴 ∈ PtFin ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		ptfinfin.1	⊢ 𝑋 = ∪ 𝐴
2	1	isptfin	⊢ ( 𝐴 ∈ PtFin → ( 𝐴 ∈ PtFin ↔ ∀ 𝑝 ∈ 𝑋 { 𝑥 ∈ 𝐴 ∣ 𝑝 ∈ 𝑥 } ∈ Fin ) )
3	2	ibi	⊢ ( 𝐴 ∈ PtFin → ∀ 𝑝 ∈ 𝑋 { 𝑥 ∈ 𝐴 ∣ 𝑝 ∈ 𝑥 } ∈ Fin )
4		eleq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∈ 𝑥 ↔ 𝑃 ∈ 𝑥 ) )
5	4	rabbidv	⊢ ( 𝑝 = 𝑃 → { 𝑥 ∈ 𝐴 ∣ 𝑝 ∈ 𝑥 } = { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } )
6	5	eleq1d	⊢ ( 𝑝 = 𝑃 → ( { 𝑥 ∈ 𝐴 ∣ 𝑝 ∈ 𝑥 } ∈ Fin ↔ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∈ Fin ) )
7	6	rspccv	⊢ ( ∀ 𝑝 ∈ 𝑋 { 𝑥 ∈ 𝐴 ∣ 𝑝 ∈ 𝑥 } ∈ Fin → ( 𝑃 ∈ 𝑋 → { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∈ Fin ) )
8	3 7	syl	⊢ ( 𝐴 ∈ PtFin → ( 𝑃 ∈ 𝑋 → { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∈ Fin ) )
9	8	imp	⊢ ( ( 𝐴 ∈ PtFin ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∈ Fin )