# 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 o. G ) : A --> C )`

### Proof

Step Hyp Ref Expression
1 df-f
` |-  ( F : B --> C <-> ( F Fn B /\ ran F C_ C ) )`
2 df-f
` |-  ( G : A --> B <-> ( G Fn A /\ ran G C_ B ) )`
3 fnco
` |-  ( ( F Fn B /\ G Fn A /\ ran G C_ B ) -> ( F o. G ) Fn A )`
4 3 3expib
` |-  ( F Fn B -> ( ( G Fn A /\ ran G C_ B ) -> ( F o. G ) Fn A ) )`
` |-  ( ( F Fn B /\ ran F C_ C ) -> ( ( G Fn A /\ ran G C_ B ) -> ( F o. G ) Fn A ) )`
6 rncoss
` |-  ran ( F o. G ) C_ ran F`
7 sstr
` |-  ( ( ran ( F o. G ) C_ ran F /\ ran F C_ C ) -> ran ( F o. G ) C_ C )`
8 6 7 mpan
` |-  ( ran F C_ C -> ran ( F o. G ) C_ C )`
` |-  ( ( F Fn B /\ ran F C_ C ) -> ran ( F o. G ) C_ C )`
` |-  ( ( F Fn B /\ ran F C_ C ) -> ( ( G Fn A /\ ran G C_ B ) -> ( ( F o. G ) Fn A /\ ran ( F o. G ) C_ C ) ) )`
` |-  ( ( ( F Fn B /\ ran F C_ C ) /\ ( G Fn A /\ ran G C_ B ) ) -> ( ( F o. G ) Fn A /\ ran ( F o. G ) C_ C ) )`
` |-  ( ( F : B --> C /\ G : A --> B ) -> ( ( F o. G ) Fn A /\ ran ( F o. G ) C_ C ) )`
` |-  ( ( F o. G ) : A --> C <-> ( ( F o. G ) Fn A /\ ran ( F o. G ) C_ C ) )`
` |-  ( ( F : B --> C /\ G : A --> B ) -> ( F o. G ) : A --> C )`