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 ) )
5 4 adantr 
 |-  ( ( 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 )
9 8 adantl 
 |-  ( ( F Fn B /\ ran F C_ C ) -> ran ( F o. G ) C_ C )
10 5 9 jctird 
 |-  ( ( 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 ) ) )
11 10 imp 
 |-  ( ( ( 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 ) )
12 1 2 11 syl2anb 
 |-  ( ( F : B --> C /\ G : A --> B ) -> ( ( F o. G ) Fn A /\ ran ( F o. G ) C_ C ) )
13 df-f 
 |-  ( ( F o. G ) : A --> C <-> ( ( F o. G ) Fn A /\ ran ( F o. G ) C_ C ) )
14 12 13 sylibr 
 |-  ( ( F : B --> C /\ G : A --> B ) -> ( F o. G ) : A --> C )