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 → F : A ⟶ onto F A

Proof

Step Hyp Ref Expression
1 fdm ⊢ F : A ⟶ B → dom ⁡ F = A
2 frel ⊢ F : A ⟶ B → Rel ⁡ F
3 resdm ⊢ Rel ⁡ F → F ↾ dom ⁡ F = F
4 3 eqcomd ⊢ Rel ⁡ F → F = F ↾ dom ⁡ F
5 2 4 syl ⊢ F : A ⟶ B → F = F ↾ dom ⁡ F
6 reseq2 ⊢ dom ⁡ F = A → F ↾ dom ⁡ F = F ↾ A
7 5 6 sylan9eq ⊢ F : A ⟶ B ∧ dom ⁡ F = A → F = F ↾ A
8 1 7 mpdan ⊢ F : A ⟶ B → F = F ↾ A
9 ffun ⊢ F : A ⟶ B → Fun ⁡ F
10 eqimss2 ⊢ dom ⁡ F = A → A ⊆ dom ⁡ F
11 1 10 syl ⊢ F : A ⟶ B → A ⊆ dom ⁡ F
12 9 11 jca ⊢ F : A ⟶ B → Fun ⁡ F ∧ A ⊆ dom ⁡ F
13 12 adantr ⊢ F : A ⟶ B ∧ F = F ↾ A → Fun ⁡ F ∧ A ⊆ dom ⁡ F
14 fores ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F → F ↾ A : A ⟶ onto F A
15 13 14 syl ⊢ F : A ⟶ B ∧ F = F ↾ A → F ↾ A : A ⟶ onto F A
16 foeq1 ⊢ F = F ↾ A → F : A ⟶ onto F A ↔ F ↾ A : A ⟶ onto F A
17 16 adantl ⊢ F : A ⟶ B ∧ F = F ↾ A → F : A ⟶ onto F A ↔ F ↾ A : A ⟶ onto F A
18 15 17 mpbird ⊢ F : A ⟶ B ∧ F = F ↾ A → F : A ⟶ onto F A
19 8 18 mpdan ⊢ F : A ⟶ B → F : A ⟶ onto F A