mptfi

Description: A finite mapping set is finite. (Contributed by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	mptfi	$⊢ A \in Fin \to (x \in A ⟼ B) \in Fin$

Step	Hyp	Ref	Expression
1		funmpt	$⊢ Fun (x \in A ⟼ B)$
2		funfn	$⊢ Fun (x \in A ⟼ B) \leftrightarrow (x \in A ⟼ B) Fn dom (x \in A ⟼ B)$
3	1 2	mpbi	$⊢ (x \in A ⟼ B) Fn dom (x \in A ⟼ B)$
4		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
5	4	dmmptss	$⊢ dom (x \in A ⟼ B) \subseteq A$
6		ssfi	$⊢ (A \in Fin \land dom (x \in A ⟼ B) \subseteq A) \to dom (x \in A ⟼ B) \in Fin$
7	5 6	mpan2	$⊢ A \in Fin \to dom (x \in A ⟼ B) \in Fin$
8		fnfi	$⊢ ((x \in A ⟼ B) Fn dom (x \in A ⟼ B) \land dom (x \in A ⟼ B) \in Fin) \to (x \in A ⟼ B) \in Fin$
9	3 7 8	sylancr	$⊢ A \in Fin \to (x \in A ⟼ B) \in Fin$

Metamath Proof Explorer