Theorem fimadmfo

Description: A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022)

	Ref	Expression
Assertion	fimadmfo	$$⊢F:A⟶B\to F:A\underset{onto}{⟶}F\left[A\right]$$

Proof

Step	Hyp	Ref	Expression
1		fdm	$$⊢F:A⟶B\to \mathrm{dom}F=A$$
2		ffn	$$⊢F:A⟶B\to FFnA$$
3	2	adantr	$$⊢\left(F:A⟶B\wedge \mathrm{dom}F=A\right)\to FFnA$$
4		dffn4	$$⊢FFnA\leftrightarrow F:A\underset{onto}{⟶}\mathrm{ran}F$$
5	3 4	sylib	$$⊢\left(F:A⟶B\wedge \mathrm{dom}F=A\right)\to F:A\underset{onto}{⟶}\mathrm{ran}F$$
6		imaeq2	$$⊢A=\mathrm{dom}F\to F\left[A\right]=F\left[\mathrm{dom}F\right]$$
7		imadmrn	$$⊢F\left[\mathrm{dom}F\right]=\mathrm{ran}F$$
8	6 7	eqtrdi	$$⊢A=\mathrm{dom}F\to F\left[A\right]=\mathrm{ran}F$$
9	8	eqcoms	$$⊢\mathrm{dom}F=A\to F\left[A\right]=\mathrm{ran}F$$
10	9	adantl	$$⊢\left(F:A⟶B\wedge \mathrm{dom}F=A\right)\to F\left[A\right]=\mathrm{ran}F$$
11		foeq3	$$⊢F\left[A\right]=\mathrm{ran}F\to \left(F:A\underset{onto}{⟶}F\left[A\right]\leftrightarrow F:A\underset{onto}{⟶}\mathrm{ran}F\right)$$
12	10 11	syl	$$⊢\left(F:A⟶B\wedge \mathrm{dom}F=A\right)\to \left(F:A\underset{onto}{⟶}F\left[A\right]\leftrightarrow F:A\underset{onto}{⟶}\mathrm{ran}F\right)$$
13	5 12	mpbird	$$⊢\left(F:A⟶B\wedge \mathrm{dom}F=A\right)\to F:A\underset{onto}{⟶}F\left[A\right]$$
14	1 13	mpdan	$$⊢F:A⟶B\to F:A\underset{onto}{⟶}F\left[A\right]$$