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 ( 𝐴 ∈ Fin → dom 𝐴 ∈ Fin )

Proof

Step Hyp Ref Expression
1 fidomdm ( 𝐴 ∈ Fin → dom 𝐴𝐴 )
2 domfi ( ( 𝐴 ∈ Fin ∧ dom 𝐴𝐴 ) → dom 𝐴 ∈ Fin )
3 1 2 mpdan ( 𝐴 ∈ Fin → dom 𝐴 ∈ Fin )