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 -> ( F e. Fin <-> dom F e. Fin ) )

Proof

Step	Hyp	Ref	Expression
1		dmfi	|- ( F e. Fin -> dom F e. Fin )
2		funfn	|- ( Fun F <-> F Fn dom F )
3		fnfi	|- ( ( F Fn dom F /\ dom F e. Fin ) -> F e. Fin )
4	2 3	sylanb	|- ( ( Fun F /\ dom F e. Fin ) -> F e. Fin )
5	4	ex	|- ( Fun F -> ( dom F e. Fin -> F e. Fin ) )
6	1 5	impbid2	|- ( Fun F -> ( F e. Fin <-> dom F e. Fin ) )