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}\leftrightarrow \forall x\in X\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}\leftrightarrow \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\left\{y\in a|x\in y\right\}\in \mathrm{Fin}\leftrightarrow \forall x\in X\left\{y\in A|x\in y\right\}\in \mathrm{Fin}\right)$$
7		df-ptfin	$$⊢\mathrm{PtFin}=\left\{a|\forall x\in \bigcup a\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}\leftrightarrow \forall x\in X\left\{y\in A|x\in y\right\}\in \mathrm{Fin}\right)$$