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 Fin dom A Fin

Proof

Step Hyp Ref Expression
1 fidomdm A Fin dom A A
2 domfi A Fin dom A A dom A Fin
3 1 2 mpdan A Fin dom A Fin