Metamath Proof Explorer

Theorem fundmfibi

Description: A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020)

		Ref	Expression
	Assertion	fundmfibi	$⊢ Fun F \to (F \in Fin \leftrightarrow dom F \in Fin)$

Step	Hyp	Ref	Expression
1		dmfi	$⊢ F \in Fin \to dom F \in Fin$
2		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
3		fnfi	$⊢ (F Fn dom F \land dom F \in Fin) \to F \in Fin$
4	2 3	sylanb	$⊢ (Fun F \land dom F \in Fin) \to F \in Fin$
5	4	ex	$⊢ Fun F \to (dom F \in Fin \to F \in Fin)$
6	1 5	impbid2	$⊢ Fun F \to (F \in Fin \leftrightarrow dom F \in Fin)$