Theorem fnco 5680

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 5669	. . . 4 |- ( F Fn A -> Fun F )
2		fnfun 5669	. . . 4 |- ( G Fn B -> Fun G )
3		funco 5617	. . . 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 1011	. 2 |- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> Fun ( F o. G ) )
6		fndm 5671	. . . . . . 7 |- ( F Fn A -> dom F = A )
7	6	sseq2d 3525	. . . . . 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 5255	. . . . 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 1010	. . 3 |- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom ( F o. G ) = dom G )
12		fndm 5671	. . . 4 |- ( G Fn B -> dom G = B )
13	12	3ad2ant2 1013	. . 3 |- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom G = B )
14	11, 13	eqtrd 2501	. 2 |- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom ( F o. G ) = B )
15		df-fn 5582	. 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 968   = wceq 1374   C_ wss 3469   dom cdm 4992   ran crn 4993   o. ccom 4996   Fun wfun 5573   Fn wfn 5574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-fun 5581  df-fn 5582

This theorem is referenced by:  fco  5732  fnfco  5741  fipreima  7815  cshco  12752  swrdco  12753  prdsinvlem  15971  prdsmgp  17036  pws1  17042  evlslem1  17948  frlmbas  18546  frlmbasOLD  18547  frlmup3  18594  frlmup4  18595  upxp  19852  uptx  19854  0vfval  25161  xppreima2  27146  sseqfv1  27954  sseqfn  27955  sseqfv2  27959  volsupnfl  29623  ftc1anclem5  29658  ftc1anclem8  29661  fourierdlem42  31404