Metamath Proof Explorer


Theorem fncoOLD

Description: Obsolete version of fnco as of 20-Sep-2024. (Contributed by NM, 22-May-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fncoOLD
|- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> ( F o. G ) Fn B )

Proof

Step Hyp Ref Expression
1 fnfun
 |-  ( F Fn A -> Fun F )
2 fnfun
 |-  ( G Fn B -> Fun G )
3 funco
 |-  ( ( Fun F /\ Fun G ) -> Fun ( F o. G ) )
4 1 2 3 syl2an
 |-  ( ( F Fn A /\ G Fn B ) -> Fun ( F o. G ) )
5 4 3adant3
 |-  ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> Fun ( F o. G ) )
6 fndm
 |-  ( F Fn A -> dom F = A )
7 6 sseq2d
 |-  ( F Fn A -> ( ran G C_ dom F <-> ran G C_ A ) )
8 7 biimpar
 |-  ( ( F Fn A /\ ran G C_ A ) -> ran G C_ dom F )
9 dmcosseq
 |-  ( ran G C_ dom F -> dom ( F o. G ) = dom G )
10 8 9 syl
 |-  ( ( F Fn A /\ ran G C_ A ) -> dom ( F o. G ) = dom G )
11 10 3adant2
 |-  ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom ( F o. G ) = dom G )
12 fndm
 |-  ( G Fn B -> dom G = B )
13 12 3ad2ant2
 |-  ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom G = B )
14 11 13 eqtrd
 |-  ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom ( F o. G ) = B )
15 df-fn
 |-  ( ( F o. G ) Fn B <-> ( Fun ( F o. G ) /\ dom ( F o. G ) = B ) )
16 5 14 15 sylanbrc
 |-  ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> ( F o. G ) Fn B )