Theorem dmfi

Description: The domain of a finite set is finite. (Contributed by Mario Carneiro, 24-Sep-2013)

	Ref	Expression
Assertion	dmfi	$$⊢A\in \mathrm{Fin}\to \mathrm{dom}A\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		fidomdm	$$⊢A\in \mathrm{Fin}\to \mathrm{dom}A\preccurlyeq A$$
2		domfi	$$⊢\left(A\in \mathrm{Fin}\wedge \mathrm{dom}A\preccurlyeq A\right)\to \mathrm{dom}A\in \mathrm{Fin}$$
3	1 2	mpdan	$$⊢A\in \mathrm{Fin}\to \mathrm{dom}A\in \mathrm{Fin}$$