Metamath Proof Explorer

Theorem foco

Description: Composition of onto functions. (Contributed by NM, 22-Mar-2006)

Ref Expression
Assertion foco ⊢ F : B ⟶ onto C ∧ G : A ⟶ onto B → F ∘ G : A ⟶ onto C

Proof

Step Hyp Ref Expression
1 dffo2 ⊢ F : B ⟶ onto C ↔ F : B ⟶ C ∧ ran ⁡ F = C
2 dffo2 ⊢ G : A ⟶ onto B ↔ G : A ⟶ B ∧ ran ⁡ G = B
3 fco ⊢ F : B ⟶ C ∧ G : A ⟶ B → F ∘ G : A ⟶ C
4 3 ad2ant2r ⊢ F : B ⟶ C ∧ ran ⁡ F = C ∧ G : A ⟶ B ∧ ran ⁡ G = B → F ∘ G : A ⟶ C
5 fdm ⊢ F : B ⟶ C → dom ⁡ F = B
6 eqtr3 ⊢ dom ⁡ F = B ∧ ran ⁡ G = B → dom ⁡ F = ran ⁡ G
7 5 6 sylan ⊢ F : B ⟶ C ∧ ran ⁡ G = B → dom ⁡ F = ran ⁡ G
8 rncoeq ⊢ dom ⁡ F = ran ⁡ G → ran ⁡ F ∘ G = ran ⁡ F
9 8 eqeq1d ⊢ dom ⁡ F = ran ⁡ G → ran ⁡ F ∘ G = C ↔ ran ⁡ F = C
10 9 biimpar ⊢ dom ⁡ F = ran ⁡ G ∧ ran ⁡ F = C → ran ⁡ F ∘ G = C
11 7 10 sylan ⊢ F : B ⟶ C ∧ ran ⁡ G = B ∧ ran ⁡ F = C → ran ⁡ F ∘ G = C
12 11 an32s ⊢ F : B ⟶ C ∧ ran ⁡ F = C ∧ ran ⁡ G = B → ran ⁡ F ∘ G = C
13 12 adantrl ⊢ F : B ⟶ C ∧ ran ⁡ F = C ∧ G : A ⟶ B ∧ ran ⁡ G = B → ran ⁡ F ∘ G = C
14 4 13 jca ⊢ F : B ⟶ C ∧ ran ⁡ F = C ∧ G : A ⟶ B ∧ ran ⁡ G = B → F ∘ G : A ⟶ C ∧ ran ⁡ F ∘ G = C
15 1 2 14 syl2anb ⊢ F : B ⟶ onto C ∧ G : A ⟶ onto B → F ∘ G : A ⟶ C ∧ ran ⁡ F ∘ G = C
16 dffo2 ⊢ F ∘ G : A ⟶ onto C ↔ F ∘ G : A ⟶ C ∧ ran ⁡ F ∘ G = C
17 15 16 sylibr ⊢ F : B ⟶ onto C ∧ G : A ⟶ onto B → F ∘ G : A ⟶ onto C