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 [A]$

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

Metamath Proof Explorer