Metamath Proof Explorer


Theorem fcoOLD

Description: Obsolete version of fco as of 20-Sep-2024. (Contributed by NM, 29-Aug-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion fcoOLD
|- ( ( 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 )