Metamath Proof Explorer

Theorem fimadmfoALT

Description: Alternate proof of fimadmfo , based on fores . A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		fdm	$⊢ F : A ⟶ B \to dom F = A$
2		frel	$⊢ F : A ⟶ B \to Rel F$
3		resdm	$⊢ Rel F \to {F ↾}_{dom F} = F$
4	3	eqcomd	$⊢ Rel F \to F = {F ↾}_{dom F}$
5	2 4	syl	$⊢ F : A ⟶ B \to F = {F ↾}_{dom F}$
6		reseq2	$⊢ dom F = A \to {F ↾}_{dom F} = {F ↾}_{A}$
7	5 6	sylan9eq	$⊢ (F : A ⟶ B \land dom F = A) \to F = {F ↾}_{A}$
8	1 7	mpdan	$⊢ F : A ⟶ B \to F = {F ↾}_{A}$
9		ffun	$⊢ F : A ⟶ B \to Fun F$
10		eqimss2	$⊢ dom F = A \to A \subseteq dom F$
11	1 10	syl	$⊢ F : A ⟶ B \to A \subseteq dom F$
12	9 11	jca	$⊢ F : A ⟶ B \to (Fun F \land A \subseteq dom F)$
13	12	adantr	$⊢ (F : A ⟶ B \land F = {F ↾}_{A}) \to (Fun F \land A \subseteq dom F)$
14		fores	$⊢ (Fun F \land A \subseteq dom F) \to ({F ↾}_{A}) : A \underset{onto}{⟶} F [A]$
15	13 14	syl	$⊢ (F : A ⟶ B \land F = {F ↾}_{A}) \to ({F ↾}_{A}) : A \underset{onto}{⟶} F [A]$
16		foeq1	$⊢ F = {F ↾}_{A} \to (F : A \underset{onto}{⟶} F [A] \leftrightarrow ({F ↾}_{A}) : A \underset{onto}{⟶} F [A])$
17	16	adantl	$⊢ (F : A ⟶ B \land F = {F ↾}_{A}) \to (F : A \underset{onto}{⟶} F [A] \leftrightarrow ({F ↾}_{A}) : A \underset{onto}{⟶} F [A])$
18	15 17	mpbird	$⊢ (F : A ⟶ B \land F = {F ↾}_{A}) \to F : A \underset{onto}{⟶} F [A]$
19	8 18	mpdan	$⊢ F : A ⟶ B \to F : A \underset{onto}{⟶} F [A]$