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	⊢ ( 𝜑 → 𝑁 ∈ Fin )
Assertion	cnvimamptfin	⊢ ( 𝜑 → ( ◡ ( 𝑝 ∈ 𝑁 ↦ 𝑋 ) “ 𝑌 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		cnvimamptfin.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
2		cnvimass	⊢ ( ◡ ( 𝑝 ∈ 𝑁 ↦ 𝑋 ) “ 𝑌 ) ⊆ dom ( 𝑝 ∈ 𝑁 ↦ 𝑋 )
3		eqid	⊢ ( 𝑝 ∈ 𝑁 ↦ 𝑋 ) = ( 𝑝 ∈ 𝑁 ↦ 𝑋 )
4	3	dmmptss	⊢ dom ( 𝑝 ∈ 𝑁 ↦ 𝑋 ) ⊆ 𝑁
5	2 4	sstri	⊢ ( ◡ ( 𝑝 ∈ 𝑁 ↦ 𝑋 ) “ 𝑌 ) ⊆ 𝑁
6		ssfi	⊢ ( ( 𝑁 ∈ Fin ∧ ( ◡ ( 𝑝 ∈ 𝑁 ↦ 𝑋 ) “ 𝑌 ) ⊆ 𝑁 ) → ( ◡ ( 𝑝 ∈ 𝑁 ↦ 𝑋 ) “ 𝑌 ) ∈ Fin )
7	1 5 6	sylancl	⊢ ( 𝜑 → ( ◡ ( 𝑝 ∈ 𝑁 ↦ 𝑋 ) “ 𝑌 ) ∈ Fin )