MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnco Structured version   Unicode version

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
StepHypRef 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 ) )
41, 2, 3syl2an 477 . . 3  |-  ( ( F  Fn  A  /\  G  Fn  B )  ->  Fun  ( F  o.  G ) )
543adant3 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 )
76sseq2d 3525 . . . . . 6  |-  ( F  Fn  A  ->  ( ran  G  C_  dom  F  <->  ran  G  C_  A ) )
87biimpar 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
)
108, 9syl 16 . . . 4  |-  ( ( F  Fn  A  /\  ran  G  C_  A )  ->  dom  ( F  o.  G )  =  dom  G )
11103adant2 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 )
13123ad2ant2 1013 . . 3  |-  ( ( F  Fn  A  /\  G  Fn  B  /\  ran  G  C_  A )  ->  dom  G  =  B )
1411, 13eqtrd 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 ) )
165, 14, 15sylanbrc 664 1  |-  ( ( F  Fn  A  /\  G  Fn  B  /\  ran  G  C_  A )  ->  ( F  o.  G
)  Fn  B )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator