This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → N ∈ Fin
Assertion cnvimamptfin ⊢ φ → p ∈ N ⟼ X -1 Y ∈ Fin

Proof

Step Hyp Ref Expression
1 cnvimamptfin.n ⊢ φ → N ∈ Fin
2 cnvimass ⊢ p ∈ N ⟼ X -1 Y ⊆ dom ⁡ p ∈ N ⟼ X
3 eqid ⊢ p ∈ N ⟼ X = p ∈ N ⟼ X
4 3 dmmptss ⊢ dom ⁡ p ∈ N ⟼ X ⊆ N
5 2 4 sstri ⊢ p ∈ N ⟼ X -1 Y ⊆ N
6 ssfi ⊢ N ∈ Fin ∧ p ∈ N ⟼ X -1 Y ⊆ N → p ∈ N ⟼ X -1 Y ∈ Fin
7 1 5 6 sylancl ⊢ φ → p ∈ N ⟼ X -1 Y ∈ Fin