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 APtFinPXxA|PxFin

Proof

Step Hyp Ref Expression
1 ptfinfin.1 X=A
2 1 isptfin APtFinAPtFinpXxA|pxFin
3 2 ibi APtFinpXxA|pxFin
4 eleq1 p=PpxPx
5 4 rabbidv p=PxA|px=xA|Px
6 5 eleq1d p=PxA|pxFinxA|PxFin
7 6 rspccv pXxA|pxFinPXxA|PxFin
8 3 7 syl APtFinPXxA|PxFin
9 8 imp APtFinPXxA|PxFin