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

Metamath Proof Explorer

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 )