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

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
StepHypRef 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 ) )
41, 2, 3syl2an 477 . . 3  |-  ( ( F  Fn  A  /\  G  Fn  B )  ->  Fun  ( F  o.  G ) )
543adant3 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 )
76sseq2d 3517 . . . . . 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 5254 . . . . 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 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 )
13123ad2ant2 1019 . . 3  |-  ( ( F  Fn  A  /\  G  Fn  B  /\  ran  G  C_  A )  ->  dom  G  =  B )
1411, 13eqtrd 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 ) )
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 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
  Copyright terms: Public domain W3C validator