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

Metamath Proof Explorer

Theorem isptfin

Description: The statement "is a point-finite cover." (Contributed by Jeff Hankins, 21-Jan-2010)

Ref Expression
Hypothesis isptfin.1 
|- X = U. A
Assertion isptfin 
|- ( A e. B -> ( A e. PtFin <-> A. x e. X { y e. A | x e. y } e. Fin ) )

Proof

Step Hyp Ref Expression
1 isptfin.1 
 |-  X = U. A
2 unieq 
 |-  ( a = A -> U. a = U. A )
3 2 1 eqtr4di 
 |-  ( a = A -> U. a = X )
4 rabeq 
 |-  ( a = A -> { y e. a | x e. y } = { y e. A | x e. y } )
5 4 eleq1d 
 |-  ( a = A -> ( { y e. a | x e. y } e. Fin <-> { y e. A | x e. y } e. Fin ) )
6 3 5 raleqbidv 
 |-  ( a = A -> ( A. x e. U. a { y e. a | x e. y } e. Fin <-> A. x e. X { y e. A | x e. y } e. Fin ) )
7 df-ptfin 
 |-  PtFin = { a | A. x e. U. a { y e. a | x e. y } e. Fin }
8 6 7 elab2g 
 |-  ( A e. B -> ( A e. PtFin <-> A. x e. X { y e. A | x e. y } e. Fin ) )