Metamath Proof Explorer


Theorem dmfi

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

Ref Expression
Assertion dmfi
|- ( A e. Fin -> dom A e. Fin )

Proof

Step Hyp Ref Expression
1 fidomdm
 |-  ( A e. Fin -> dom A ~<_ A )
2 domfi
 |-  ( ( A e. Fin /\ dom A ~<_ A ) -> dom A e. Fin )
3 1 2 mpdan
 |-  ( A e. Fin -> dom A e. Fin )