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 = U. A
Assertion ptfinfin 
|- ( ( A e. PtFin /\ P e. X ) -> { x e. A | P e. x } e. Fin )

Proof

Step Hyp Ref Expression
1 ptfinfin.1 
 |-  X = U. A
2 1 isptfin 
 |-  ( A e. PtFin -> ( A e. PtFin <-> A. p e. X { x e. A | p e. x } e. Fin ) )
3 2 ibi 
 |-  ( A e. PtFin -> A. p e. X { x e. A | p e. x } e. Fin )
4 eleq1 
 |-  ( p = P -> ( p e. x <-> P e. x ) )
5 4 rabbidv 
 |-  ( p = P -> { x e. A | p e. x } = { x e. A | P e. x } )
6 5 eleq1d 
 |-  ( p = P -> ( { x e. A | p e. x } e. Fin <-> { x e. A | P e. x } e. Fin ) )
7 6 rspccv 
 |-  ( A. p e. X { x e. A | p e. x } e. Fin -> ( P e. X -> { x e. A | P e. x } e. Fin ) )
8 3 7 syl 
 |-  ( A e. PtFin -> ( P e. X -> { x e. A | P e. x } e. Fin ) )
9 8 imp 
 |-  ( ( A e. PtFin /\ P e. X ) -> { x e. A | P e. x } e. Fin )