Metamath Proof Explorer

Theorem focofo

Description: Composition of onto functions. Generalisation of foco . (Contributed by AV, 29-Sep-2024)

Ref Expression
Assertion focofo ⊢ F : A ⟶ onto B ∧ Fun ⁡ G ∧ A ⊆ ran ⁡ G → F ∘ G : G -1 A ⟶ onto B

Proof

Step Hyp Ref Expression
1 fof ⊢ F : A ⟶ onto B → F : A ⟶ B
2 fcof ⊢ F : A ⟶ B ∧ Fun ⁡ G → F ∘ G : G -1 A ⟶ B
3 1 2 sylan ⊢ F : A ⟶ onto B ∧ Fun ⁡ G → F ∘ G : G -1 A ⟶ B
4 3 3adant3 ⊢ F : A ⟶ onto B ∧ Fun ⁡ G ∧ A ⊆ ran ⁡ G → F ∘ G : G -1 A ⟶ B
5 rnco ⊢ ran ⁡ F ∘ G = ran ⁡ F ↾ ran ⁡ G
6 1 freld ⊢ F : A ⟶ onto B → Rel ⁡ F
7 6 3ad2ant1 ⊢ F : A ⟶ onto B ∧ Fun ⁡ G ∧ A ⊆ ran ⁡ G → Rel ⁡ F
8 fdm ⊢ F : A ⟶ B → dom ⁡ F = A
9 8 eqcomd ⊢ F : A ⟶ B → A = dom ⁡ F
10 1 9 syl ⊢ F : A ⟶ onto B → A = dom ⁡ F
11 10 sseq1d ⊢ F : A ⟶ onto B → A ⊆ ran ⁡ G ↔ dom ⁡ F ⊆ ran ⁡ G
12 11 biimpa ⊢ F : A ⟶ onto B ∧ A ⊆ ran ⁡ G → dom ⁡ F ⊆ ran ⁡ G
13 relssres ⊢ Rel ⁡ F ∧ dom ⁡ F ⊆ ran ⁡ G → F ↾ ran ⁡ G = F
14 13 rneqd ⊢ Rel ⁡ F ∧ dom ⁡ F ⊆ ran ⁡ G → ran ⁡ F ↾ ran ⁡ G = ran ⁡ F
15 7 12 14 3imp3i2an ⊢ F : A ⟶ onto B ∧ Fun ⁡ G ∧ A ⊆ ran ⁡ G → ran ⁡ F ↾ ran ⁡ G = ran ⁡ F
16 forn ⊢ F : A ⟶ onto B → ran ⁡ F = B
17 16 3ad2ant1 ⊢ F : A ⟶ onto B ∧ Fun ⁡ G ∧ A ⊆ ran ⁡ G → ran ⁡ F = B
18 15 17 eqtrd ⊢ F : A ⟶ onto B ∧ Fun ⁡ G ∧ A ⊆ ran ⁡ G → ran ⁡ F ↾ ran ⁡ G = B
19 5 18 eqtrid ⊢ F : A ⟶ onto B ∧ Fun ⁡ G ∧ A ⊆ ran ⁡ G → ran ⁡ F ∘ G = B
20 dffo2 ⊢ F ∘ G : G -1 A ⟶ onto B ↔ F ∘ G : G -1 A ⟶ B ∧ ran ⁡ F ∘ G = B
21 4 19 20 sylanbrc ⊢ F : A ⟶ onto B ∧ Fun ⁡ G ∧ A ⊆ ran ⁡ G → F ∘ G : G -1 A ⟶ onto B