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 )