Theorem fnco 5679

Description: Composition of two functions. (Contributed by NM, 22-May-2006.)

Assertion

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

Proof of Theorem fnco

Step	Hyp	Ref	Expression
1		fnfun 5668	. . . 4 |- ( F Fn A -> Fun F )
2		fnfun 5668	. . . 4 |- ( G Fn B -> Fun G )
3		funco 5616	. . . 4 |- ( ( Fun F /\ Fun G ) -> Fun ( F o. G ) )
4	1, 2, 3	syl2an 477	. . 3 |- ( ( F Fn A /\ G Fn B ) -> Fun ( F o. G ) )
5	4	3adant3 1017	. 2 |- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> Fun ( F o. G ) )
6		fndm 5670	. . . . . . 7 |- ( F Fn A -> dom F = A )
7	6	sseq2d 3517	. . . . . 6 |- ( F Fn A -> ( ran G C_ dom F <-> ran G C_ A ) )
8	7	biimpar 485	. . . . 5 |- ( ( F Fn A /\ ran G C_ A ) -> ran G C_ dom F )
9		dmcosseq 5254	. . . . 5 |- ( ran G C_ dom F -> dom ( F o. G ) = dom G )
10	8, 9	syl 16	. . . 4 |- ( ( F Fn A /\ ran G C_ A ) -> dom ( F o. G ) = dom G )
11	10	3adant2 1016	. . 3 |- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom ( F o. G ) = dom G )
12		fndm 5670	. . . 4 |- ( G Fn B -> dom G = B )
13	12	3ad2ant2 1019	. . 3 |- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom G = B )
14	11, 13	eqtrd 2484	. 2 |- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom ( F o. G ) = B )
15		df-fn 5581	. 2 |- ( ( F o. G ) Fn B <-> ( Fun ( F o. G ) /\ dom ( F o. G ) = B ) )
16	5, 14, 15	sylanbrc 664	1 |- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> ( F o. G ) Fn B )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 974   = wceq 1383   C_ wss 3461   dom cdm 4989   ran crn 4990   o. ccom 4993   Fun wfun 5572   Fn wfn 5573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-fun 5580  df-fn 5581

This theorem is referenced by:  fco  5731  fnfco  5740  fipreima  7828  cshco  12784  swrdco  12785  prdsinvlem  16157  prdsmgp  17238  pws1  17244  evlslem1  18163  frlmbas  18764  frlmbasOLD  18765  frlmup3  18812  frlmup4  18813  upxp  20102  uptx  20104  0vfval  25477  xppreima2  27466  sseqfv1  28306  sseqfn  28307  sseqfv2  28311  volsupnfl  30035  ftc1anclem5  30070  ftc1anclem8  30073  fourierdlem42  31885