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 ⊢ X = ⋃ A
Assertion ptfinfin ⊢ A ∈ PtFin ∧ P ∈ X → x ∈ A | P ∈ x ∈ Fin

Proof

Step Hyp Ref Expression
1 ptfinfin.1 ⊢ X = ⋃ A
2 1 isptfin ⊢ A ∈ PtFin → A ∈ PtFin ↔ ∀ p ∈ X x ∈ A | p ∈ x ∈ Fin
3 2 ibi ⊢ A ∈ PtFin → ∀ p ∈ X x ∈ A | p ∈ x ∈ Fin
4 eleq1 ⊢ p = P → p ∈ x ↔ P ∈ x
5 4 rabbidv ⊢ p = P → x ∈ A | p ∈ x = x ∈ A | P ∈ x
6 5 eleq1d ⊢ p = P → x ∈ A | p ∈ x ∈ Fin ↔ x ∈ A | P ∈ x ∈ Fin
7 6 rspccv ⊢ ∀ p ∈ X x ∈ A | p ∈ x ∈ Fin → P ∈ X → x ∈ A | P ∈ x ∈ Fin
8 3 7 syl ⊢ A ∈ PtFin → P ∈ X → x ∈ A | P ∈ x ∈ Fin
9 8 imp ⊢ A ∈ PtFin ∧ P ∈ X → x ∈ A | P ∈ x ∈ Fin