Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Finite sets (cont.)
dmfi
Next ⟩
fundmfibi
Metamath Proof Explorer
Ascii
Unicode
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