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

Proof

Step	Hyp	Ref	Expression
1		dmfi	⊢ ( 𝐹 ∈ Fin → dom 𝐹 ∈ Fin )
2		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
3		fnfi	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ dom 𝐹 ∈ Fin ) → 𝐹 ∈ Fin )
4	2 3	sylanb	⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ∈ Fin ) → 𝐹 ∈ Fin )
5	4	ex	⊢ ( Fun 𝐹 → ( dom 𝐹 ∈ Fin → 𝐹 ∈ Fin ) )
6	1 5	impbid2	⊢ ( Fun 𝐹 → ( 𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin ) )