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 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