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

Theorem fnfco 5762
Description: Composition of two functions. (Contributed by NM, 22-May-2006.)
Assertion
Ref Expression
fnfco  |-  ( ( F  Fn  A  /\  G : B --> A )  ->  ( F  o.  G )  Fn  B
)

Proof of Theorem fnfco
StepHypRef Expression
1 df-f 5602 . 2  |-  ( G : B --> A  <->  ( G  Fn  B  /\  ran  G  C_  A ) )
2 fnco 5699 . . 3  |-  ( ( F  Fn  A  /\  G  Fn  B  /\  ran  G  C_  A )  ->  ( F  o.  G
)  Fn  B )
323expb 1206 . 2  |-  ( ( F  Fn  A  /\  ( G  Fn  B  /\  ran  G  C_  A
) )  ->  ( F  o.  G )  Fn  B )
41, 3sylan2b 477 1  |-  ( ( F  Fn  A  /\  G : B --> A )  ->  ( F  o.  G )  Fn  B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    C_ wss 3436   ran crn 4851    o. ccom 4854    Fn wfn 5593   -->wf 5594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-fun 5600  df-fn 5601  df-f 5602
This theorem is referenced by:  cocan1  6201  cocan2  6202  ofco  6562  1stcof  6832  2ndcof  6833  axcc3  8869  dmaf  15932  cdaf  15933  gsumzaddlem  17542  prdstopn  20630  xpstopnlem2  20813  prdstgpd  21126  prdsxmslem2  21531  uniiccdif  22522  uniiccvol  22524  uniioombllem2  22527  uniioombllem2OLD  22528  resinf1o  23472  jensen  23901  occllem  26942  nlelchi  27700  hmopidmchi  27790  iprodefisumlem  30371  stoweidlem27  37707
  Copyright terms: Public domain W3C validator