Theorem cnvimamptfin

Description: A preimage of a mapping with a finite domain under any class is finite. In contrast to fisuppfi , the range of the mapping needs not to be known. (Contributed by AV, 21-Dec-2018)

	Ref	Expression
Hypothesis	cnvimamptfin.n	$$⊢\phi \to N\in \mathrm{Fin}$$
Assertion	cnvimamptfin	$$⊢\phi \to {\left(p\in N⟼X\right)}^{-1}\left[Y\right]\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		cnvimamptfin.n	$$⊢\phi \to N\in \mathrm{Fin}$$
2		cnvimass	$$⊢{\left(p\in N⟼X\right)}^{-1}\left[Y\right]\subseteq \mathrm{dom}\left(p\in N⟼X\right)$$
3		eqid	$$⊢\left(p\in N⟼X\right)=\left(p\in N⟼X\right)$$
4	3	dmmptss	$$⊢\mathrm{dom}\left(p\in N⟼X\right)\subseteq N$$
5	2 4	sstri	$$⊢{\left(p\in N⟼X\right)}^{-1}\left[Y\right]\subseteq N$$
6		ssfi	$$⊢\left(N\in \mathrm{Fin}\wedge {\left(p\in N⟼X\right)}^{-1}\left[Y\right]\subseteq N\right)\to {\left(p\in N⟼X\right)}^{-1}\left[Y\right]\in \mathrm{Fin}$$
7	1 5 6	sylancl	$$⊢\phi \to {\left(p\in N⟼X\right)}^{-1}\left[Y\right]\in \mathrm{Fin}$$