# 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}=\bigcup {A}$
Assertion isptfin ${⊢}{A}\in {B}\to \left({A}\in \mathrm{PtFin}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {A}|{x}\in {y}\right\}\in \mathrm{Fin}\right)$

### Proof

Step Hyp Ref Expression
1 isptfin.1 ${⊢}{X}=\bigcup {A}$
2 unieq ${⊢}{a}={A}\to \bigcup {a}=\bigcup {A}$
3 2 1 eqtr4di ${⊢}{a}={A}\to \bigcup {a}={X}$
4 rabeq ${⊢}{a}={A}\to \left\{{y}\in {a}|{x}\in {y}\right\}=\left\{{y}\in {A}|{x}\in {y}\right\}$
5 4 eleq1d ${⊢}{a}={A}\to \left(\left\{{y}\in {a}|{x}\in {y}\right\}\in \mathrm{Fin}↔\left\{{y}\in {A}|{x}\in {y}\right\}\in \mathrm{Fin}\right)$
6 3 5 raleqbidv ${⊢}{a}={A}\to \left(\forall {x}\in \bigcup {a}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {a}|{x}\in {y}\right\}\in \mathrm{Fin}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {A}|{x}\in {y}\right\}\in \mathrm{Fin}\right)$
7 df-ptfin ${⊢}\mathrm{PtFin}=\left\{{a}|\forall {x}\in \bigcup {a}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {a}|{x}\in {y}\right\}\in \mathrm{Fin}\right\}$
8 6 7 elab2g ${⊢}{A}\in {B}\to \left({A}\in \mathrm{PtFin}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {A}|{x}\in {y}\right\}\in \mathrm{Fin}\right)$