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	|- ( ph -> N e. Fin )
Assertion	cnvimamptfin	|- ( ph -> ( `' ( p e. N |-> X ) " Y ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		cnvimamptfin.n	|- ( ph -> N e. Fin )
2		cnvimass	|- ( `' ( p e. N |-> X ) " Y ) C_ dom ( p e. N |-> X )
3		eqid	|- ( p e. N |-> X ) = ( p e. N |-> X )
4	3	dmmptss	|- dom ( p e. N |-> X ) C_ N
5	2 4	sstri	|- ( `' ( p e. N |-> X ) " Y ) C_ N
6		ssfi	|- ( ( N e. Fin /\ ( `' ( p e. N |-> X ) " Y ) C_ N ) -> ( `' ( p e. N |-> X ) " Y ) e. Fin )
7	1 5 6	sylancl	|- ( ph -> ( `' ( p e. N |-> X ) " Y ) e. Fin )