# Metamath Proof Explorer

## Theorem fco

Description: Composition of two mappings. (Contributed by NM, 29-Aug-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion fco $⊢ F : B ⟶ C ∧ G : A ⟶ B → F ∘ G : A ⟶ C$

### Proof

Step Hyp Ref Expression
1 df-f $⊢ F : B ⟶ C ↔ F Fn B ∧ ran ⁡ F ⊆ C$
2 df-f $⊢ G : A ⟶ B ↔ G Fn A ∧ ran ⁡ G ⊆ B$
3 fnco $⊢ F Fn B ∧ G Fn A ∧ ran ⁡ G ⊆ B → F ∘ G Fn A$
4 3 3expib $⊢ F Fn B → G Fn A ∧ ran ⁡ G ⊆ B → F ∘ G Fn A$
5 4 adantr $⊢ F Fn B ∧ ran ⁡ F ⊆ C → G Fn A ∧ ran ⁡ G ⊆ B → F ∘ G Fn A$
6 rncoss $⊢ ran ⁡ F ∘ G ⊆ ran ⁡ F$
7 sstr $⊢ ran ⁡ F ∘ G ⊆ ran ⁡ F ∧ ran ⁡ F ⊆ C → ran ⁡ F ∘ G ⊆ C$
8 6 7 mpan $⊢ ran ⁡ F ⊆ C → ran ⁡ F ∘ G ⊆ C$
9 8 adantl $⊢ F Fn B ∧ ran ⁡ F ⊆ C → ran ⁡ F ∘ G ⊆ C$
10 5 9 jctird $⊢ F Fn B ∧ ran ⁡ F ⊆ C → G Fn A ∧ ran ⁡ G ⊆ B → F ∘ G Fn A ∧ ran ⁡ F ∘ G ⊆ C$
11 10 imp $⊢ F Fn B ∧ ran ⁡ F ⊆ C ∧ G Fn A ∧ ran ⁡ G ⊆ B → F ∘ G Fn A ∧ ran ⁡ F ∘ G ⊆ C$
12 1 2 11 syl2anb $⊢ F : B ⟶ C ∧ G : A ⟶ B → F ∘ G Fn A ∧ ran ⁡ F ∘ G ⊆ C$
13 df-f $⊢ F ∘ G : A ⟶ C ↔ F ∘ G Fn A ∧ ran ⁡ F ∘ G ⊆ C$
14 12 13 sylibr $⊢ F : B ⟶ C ∧ G : A ⟶ B → F ∘ G : A ⟶ C$