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

Theorem fcompt 5878
Description: Express composition of two functions as a maps-to applying both in sequence. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
Assertion
Ref Expression
fcompt  |-  ( ( A : D --> E  /\  B : C --> D )  ->  ( A  o.  B )  =  ( x  e.  C  |->  ( A `  ( B `
 x ) ) ) )
Distinct variable groups:    x, A    x, B    x, C    x, D    x, E

Proof of Theorem fcompt
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 ffvelrn 5840 . . 3  |-  ( ( B : C --> D  /\  x  e.  C )  ->  ( B `  x
)  e.  D )
21adantll 713 . 2  |-  ( ( ( A : D --> E  /\  B : C --> D )  /\  x  e.  C )  ->  ( B `  x )  e.  D )
3 ffn 5558 . . . 4  |-  ( B : C --> D  ->  B  Fn  C )
43adantl 466 . . 3  |-  ( ( A : D --> E  /\  B : C --> D )  ->  B  Fn  C
)
5 dffn5 5736 . . 3  |-  ( B  Fn  C  <->  B  =  ( x  e.  C  |->  ( B `  x
) ) )
64, 5sylib 196 . 2  |-  ( ( A : D --> E  /\  B : C --> D )  ->  B  =  ( x  e.  C  |->  ( B `  x ) ) )
7 ffn 5558 . . . 4  |-  ( A : D --> E  ->  A  Fn  D )
87adantr 465 . . 3  |-  ( ( A : D --> E  /\  B : C --> D )  ->  A  Fn  D
)
9 dffn5 5736 . . 3  |-  ( A  Fn  D  <->  A  =  ( y  e.  D  |->  ( A `  y
) ) )
108, 9sylib 196 . 2  |-  ( ( A : D --> E  /\  B : C --> D )  ->  A  =  ( y  e.  D  |->  ( A `  y ) ) )
11 fveq2 5690 . 2  |-  ( y  =  ( B `  x )  ->  ( A `  y )  =  ( A `  ( B `  x ) ) )
122, 6, 10, 11fmptco 5875 1  |-  ( ( A : D --> E  /\  B : C --> D )  ->  ( A  o.  B )  =  ( x  e.  C  |->  ( A `  ( B `
 x ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756    e. cmpt 4349    o. ccom 4843    Fn wfn 5412   -->wf 5413   ` cfv 5417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-nul 4420  ax-pow 4469  ax-pr 4530
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2719  df-rex 2720  df-rab 2723  df-v 2973  df-sbc 3186  df-csb 3288  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-uni 4091  df-br 4292  df-opab 4350  df-mpt 4351  df-id 4635  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-fv 5425
This theorem is referenced by:  revco  12461  repsco  12466  caucvgrlem2  13151  fucidcl  14874  fucsect  14881  prf1st  15013  prf2nd  15014  curfcl  15041  yonedalem4c  15086  yonedalem3b  15088  yonedainv  15090  frmdup3  15543  efginvrel1  16224  frgpup3lem  16273  frgpup3  16274  dprdfinv  16508  dprdfinvOLD  16515  grpvlinv  18294  grpvrinv  18295  mhmvlin  18296  prdstps  19201  imasdsf1olem  19947  meascnbl  26632  gamcvg2lem  27044  mzprename  29084  mendassa  29549  mulc1cncfg  29768  expcnfg  29771
  Copyright terms: Public domain W3C validator