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

Theorem fmptco 5904
Description: Composition of two functions expressed as ordered-pair class abstractions. If  F has the equation  ( x  +  2 ) and  G the equation  ( 3 * z ) then  ( G  o.  F ) has the equation  ( 3
* ( x  + 
2 ) ). (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.)
Hypotheses
Ref Expression
fmptco.1  |-  ( (
ph  /\  x  e.  A )  ->  R  e.  B )
fmptco.2  |-  ( ph  ->  F  =  ( x  e.  A  |->  R ) )
fmptco.3  |-  ( ph  ->  G  =  ( y  e.  B  |->  S ) )
fmptco.4  |-  ( y  =  R  ->  S  =  T )
Assertion
Ref Expression
fmptco  |-  ( ph  ->  ( G  o.  F
)  =  ( x  e.  A  |->  T ) )
Distinct variable groups:    x, A    x, y, B    y, R    ph, x    x, S    y, T
Allowed substitution hints:    ph( y)    A( y)    R( x)    S( y)    T( x)    F( x, y)    G( x, y)

Proof of Theorem fmptco
Dummy variables  v  u  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relco 5371 . 2  |-  Rel  ( G  o.  F )
2 funmpt 5492 . . 3  |-  Fun  (
x  e.  A  |->  T )
3 funrel 5474 . . 3  |-  ( Fun  ( x  e.  A  |->  T )  ->  Rel  ( x  e.  A  |->  T ) )
42, 3ax-mp 5 . 2  |-  Rel  (
x  e.  A  |->  T )
5 fmptco.1 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  R  e.  B )
6 eqid 2438 . . . . . . . . . . . . 13  |-  ( x  e.  A  |->  R )  =  ( x  e.  A  |->  R )
75, 6fmptd 5896 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  A  |->  R ) : A --> B )
8 fmptco.2 . . . . . . . . . . . . 13  |-  ( ph  ->  F  =  ( x  e.  A  |->  R ) )
98feq1d 5583 . . . . . . . . . . . 12  |-  ( ph  ->  ( F : A --> B 
<->  ( x  e.  A  |->  R ) : A --> B ) )
107, 9mpbird 225 . . . . . . . . . . 11  |-  ( ph  ->  F : A --> B )
11 ffun 5596 . . . . . . . . . . 11  |-  ( F : A --> B  ->  Fun  F )
1210, 11syl 16 . . . . . . . . . 10  |-  ( ph  ->  Fun  F )
13 funbrfv 5768 . . . . . . . . . . 11  |-  ( Fun 
F  ->  ( z F u  ->  ( F `
 z )  =  u ) )
1413imp 420 . . . . . . . . . 10  |-  ( ( Fun  F  /\  z F u )  -> 
( F `  z
)  =  u )
1512, 14sylan 459 . . . . . . . . 9  |-  ( (
ph  /\  z F u )  ->  ( F `  z )  =  u )
1615eqcomd 2443 . . . . . . . 8  |-  ( (
ph  /\  z F u )  ->  u  =  ( F `  z ) )
1716a1d 24 . . . . . . 7  |-  ( (
ph  /\  z F u )  ->  (
u G w  ->  u  =  ( F `  z ) ) )
1817expimpd 588 . . . . . 6  |-  ( ph  ->  ( ( z F u  /\  u G w )  ->  u  =  ( F `  z ) ) )
1918pm4.71rd 618 . . . . 5  |-  ( ph  ->  ( ( z F u  /\  u G w )  <->  ( u  =  ( F `  z )  /\  (
z F u  /\  u G w ) ) ) )
2019exbidv 1637 . . . 4  |-  ( ph  ->  ( E. u ( z F u  /\  u G w )  <->  E. u
( u  =  ( F `  z )  /\  ( z F u  /\  u G w ) ) ) )
21 fvex 5745 . . . . . 6  |-  ( F `
 z )  e. 
_V
22 breq2 4219 . . . . . . 7  |-  ( u  =  ( F `  z )  ->  (
z F u  <->  z F
( F `  z
) ) )
23 breq1 4218 . . . . . . 7  |-  ( u  =  ( F `  z )  ->  (
u G w  <->  ( F `  z ) G w ) )
2422, 23anbi12d 693 . . . . . 6  |-  ( u  =  ( F `  z )  ->  (
( z F u  /\  u G w )  <->  ( z F ( F `  z
)  /\  ( F `  z ) G w ) ) )
2521, 24ceqsexv 2993 . . . . 5  |-  ( E. u ( u  =  ( F `  z
)  /\  ( z F u  /\  u G w ) )  <-> 
( z F ( F `  z )  /\  ( F `  z ) G w ) )
26 funfvbrb 5846 . . . . . . . . 9  |-  ( Fun 
F  ->  ( z  e.  dom  F  <->  z F
( F `  z
) ) )
2712, 26syl 16 . . . . . . . 8  |-  ( ph  ->  ( z  e.  dom  F  <-> 
z F ( F `
 z ) ) )
28 fdm 5598 . . . . . . . . . 10  |-  ( F : A --> B  ->  dom  F  =  A )
2910, 28syl 16 . . . . . . . . 9  |-  ( ph  ->  dom  F  =  A )
3029eleq2d 2505 . . . . . . . 8  |-  ( ph  ->  ( z  e.  dom  F  <-> 
z  e.  A ) )
3127, 30bitr3d 248 . . . . . . 7  |-  ( ph  ->  ( z F ( F `  z )  <-> 
z  e.  A ) )
328fveq1d 5733 . . . . . . . 8  |-  ( ph  ->  ( F `  z
)  =  ( ( x  e.  A  |->  R ) `  z ) )
33 fmptco.3 . . . . . . . 8  |-  ( ph  ->  G  =  ( y  e.  B  |->  S ) )
34 eqidd 2439 . . . . . . . 8  |-  ( ph  ->  w  =  w )
3532, 33, 34breq123d 4229 . . . . . . 7  |-  ( ph  ->  ( ( F `  z ) G w  <-> 
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w ) )
3631, 35anbi12d 693 . . . . . 6  |-  ( ph  ->  ( ( z F ( F `  z
)  /\  ( F `  z ) G w )  <->  ( z  e.  A  /\  ( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w ) ) )
37 nfcv 2574 . . . . . . . . 9  |-  F/_ x
z
38 nfv 1630 . . . . . . . . . 10  |-  F/ x ph
39 nffvmpt1 5739 . . . . . . . . . . . 12  |-  F/_ x
( ( x  e.  A  |->  R ) `  z )
40 nfcv 2574 . . . . . . . . . . . 12  |-  F/_ x
( y  e.  B  |->  S )
41 nfcv 2574 . . . . . . . . . . . 12  |-  F/_ x w
4239, 40, 41nfbr 4259 . . . . . . . . . . 11  |-  F/ x
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w
43 nfcsb1v 3285 . . . . . . . . . . . 12  |-  F/_ x [_ z  /  x ]_ T
4443nfeq2 2585 . . . . . . . . . . 11  |-  F/ x  w  =  [_ z  /  x ]_ T
4542, 44nfbi 1857 . . . . . . . . . 10  |-  F/ x
( ( ( x  e.  A  |->  R ) `
 z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T )
4638, 45nfim 1833 . . . . . . . . 9  |-  F/ x
( ph  ->  ( ( ( x  e.  A  |->  R ) `  z
) ( y  e.  B  |->  S ) w  <-> 
w  =  [_ z  /  x ]_ T ) )
47 fveq2 5731 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( x  e.  A  |->  R ) `  x
)  =  ( ( x  e.  A  |->  R ) `  z ) )
4847breq1d 4225 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  ( ( x  e.  A  |->  R ) `
 z ) ( y  e.  B  |->  S ) w ) )
49 csbeq1a 3261 . . . . . . . . . . . 12  |-  ( x  =  z  ->  T  =  [_ z  /  x ]_ T )
5049eqeq2d 2449 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
w  =  T  <->  w  =  [_ z  /  x ]_ T ) )
5148, 50bibi12d 314 . . . . . . . . . 10  |-  ( x  =  z  ->  (
( ( ( x  e.  A  |->  R ) `
 x ) ( y  e.  B  |->  S ) w  <->  w  =  T )  <->  ( (
( x  e.  A  |->  R ) `  z
) ( y  e.  B  |->  S ) w  <-> 
w  =  [_ z  /  x ]_ T ) ) )
5251imbi2d 309 . . . . . . . . 9  |-  ( x  =  z  ->  (
( ph  ->  ( ( ( x  e.  A  |->  R ) `  x
) ( y  e.  B  |->  S ) w  <-> 
w  =  T ) )  <->  ( ph  ->  ( ( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T ) ) ) )
53 vex 2961 . . . . . . . . . . . 12  |-  w  e. 
_V
54 simpl 445 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  y  =  R )
5554eleq1d 2504 . . . . . . . . . . . . . 14  |-  ( ( y  =  R  /\  u  =  w )  ->  ( y  e.  B  <->  R  e.  B ) )
56 simpr 449 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  u  =  w )
57 fmptco.4 . . . . . . . . . . . . . . . 16  |-  ( y  =  R  ->  S  =  T )
5857adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  S  =  T )
5956, 58eqeq12d 2452 . . . . . . . . . . . . . 14  |-  ( ( y  =  R  /\  u  =  w )  ->  ( u  =  S  <-> 
w  =  T ) )
6055, 59anbi12d 693 . . . . . . . . . . . . 13  |-  ( ( y  =  R  /\  u  =  w )  ->  ( ( y  e.  B  /\  u  =  S )  <->  ( R  e.  B  /\  w  =  T ) ) )
61 df-mpt 4271 . . . . . . . . . . . . 13  |-  ( y  e.  B  |->  S )  =  { <. y ,  u >.  |  (
y  e.  B  /\  u  =  S ) }
6260, 61brabga 4472 . . . . . . . . . . . 12  |-  ( ( R  e.  B  /\  w  e.  _V )  ->  ( R ( y  e.  B  |->  S ) w  <->  ( R  e.  B  /\  w  =  T ) ) )
635, 53, 62sylancl 645 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ( R ( y  e.  B  |->  S ) w  <-> 
( R  e.  B  /\  w  =  T
) ) )
64 simpr 449 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
656fvmpt2 5815 . . . . . . . . . . . . 13  |-  ( ( x  e.  A  /\  R  e.  B )  ->  ( ( x  e.  A  |->  R ) `  x )  =  R )
6664, 5, 65syl2anc 644 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  R ) `  x
)  =  R )
6766breq1d 4225 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  R ( y  e.  B  |->  S ) w ) )
685biantrurd 496 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
w  =  T  <->  ( R  e.  B  /\  w  =  T ) ) )
6963, 67, 683bitr4d 278 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  w  =  T
) )
7069expcom 426 . . . . . . . . 9  |-  ( x  e.  A  ->  ( ph  ->  ( ( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  w  =  T ) ) )
7137, 46, 52, 70vtoclgaf 3018 . . . . . . . 8  |-  ( z  e.  A  ->  ( ph  ->  ( ( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T ) ) )
7271impcom 421 . . . . . . 7  |-  ( (
ph  /\  z  e.  A )  ->  (
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T ) )
7372pm5.32da 624 . . . . . 6  |-  ( ph  ->  ( ( z  e.  A  /\  ( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w )  <-> 
( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
7436, 73bitrd 246 . . . . 5  |-  ( ph  ->  ( ( z F ( F `  z
)  /\  ( F `  z ) G w )  <->  ( z  e.  A  /\  w  = 
[_ z  /  x ]_ T ) ) )
7525, 74syl5bb 250 . . . 4  |-  ( ph  ->  ( E. u ( u  =  ( F `
 z )  /\  ( z F u  /\  u G w ) )  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
7620, 75bitrd 246 . . 3  |-  ( ph  ->  ( E. u ( z F u  /\  u G w )  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
77 vex 2961 . . . 4  |-  z  e. 
_V
7877, 53opelco 5047 . . 3  |-  ( <.
z ,  w >.  e.  ( G  o.  F
)  <->  E. u ( z F u  /\  u G w ) )
79 df-mpt 4271 . . . . 5  |-  ( x  e.  A  |->  T )  =  { <. x ,  v >.  |  ( x  e.  A  /\  v  =  T ) }
8079eleq2i 2502 . . . 4  |-  ( <.
z ,  w >.  e.  ( x  e.  A  |->  T )  <->  <. z ,  w >.  e.  { <. x ,  v >.  |  ( x  e.  A  /\  v  =  T ) } )
81 nfv 1630 . . . . . 6  |-  F/ x  z  e.  A
8243nfeq2 2585 . . . . . 6  |-  F/ x  v  =  [_ z  /  x ]_ T
8381, 82nfan 1847 . . . . 5  |-  F/ x
( z  e.  A  /\  v  =  [_ z  /  x ]_ T )
84 nfv 1630 . . . . 5  |-  F/ v ( z  e.  A  /\  w  =  [_ z  /  x ]_ T )
85 eleq1 2498 . . . . . 6  |-  ( x  =  z  ->  (
x  e.  A  <->  z  e.  A ) )
8649eqeq2d 2449 . . . . . 6  |-  ( x  =  z  ->  (
v  =  T  <->  v  =  [_ z  /  x ]_ T ) )
8785, 86anbi12d 693 . . . . 5  |-  ( x  =  z  ->  (
( x  e.  A  /\  v  =  T
)  <->  ( z  e.  A  /\  v  = 
[_ z  /  x ]_ T ) ) )
88 eqeq1 2444 . . . . . 6  |-  ( v  =  w  ->  (
v  =  [_ z  /  x ]_ T  <->  w  =  [_ z  /  x ]_ T ) )
8988anbi2d 686 . . . . 5  |-  ( v  =  w  ->  (
( z  e.  A  /\  v  =  [_ z  /  x ]_ T )  <-> 
( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
9083, 84, 77, 53, 87, 89opelopabf 4482 . . . 4  |-  ( <.
z ,  w >.  e. 
{ <. x ,  v
>.  |  ( x  e.  A  /\  v  =  T ) }  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) )
9180, 90bitri 242 . . 3  |-  ( <.
z ,  w >.  e.  ( x  e.  A  |->  T )  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) )
9276, 78, 913bitr4g 281 . 2  |-  ( ph  ->  ( <. z ,  w >.  e.  ( G  o.  F )  <->  <. z ,  w >.  e.  (
x  e.  A  |->  T ) ) )
931, 4, 92eqrelrdv 4975 1  |-  ( ph  ->  ( G  o.  F
)  =  ( x  e.  A  |->  T ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360   E.wex 1551    = wceq 1653    e. wcel 1726   _Vcvv 2958   [_csb 3253   <.cop 3819   class class class wbr 4215   {copab 4268    e. cmpt 4269   dom cdm 4881    o. ccom 4885   Rel wrel 4886   Fun wfun 5451   -->wf 5453   ` cfv 5457
This theorem is referenced by:  fmptcof  5905  fcompt  5907  fcoconst  5908  ofco  6327  ccatco  11809  lo1o12  12332  rlimcn1  12387  rlimcn1b  12388  rlimdiv  12444  ackbijnn  12612  setcepi  14248  prf1st  14306  prf2nd  14307  hofcllem  14360  prdsidlem  14732  pws0g  14736  pwsco1mhm  14774  pwsco2mhm  14775  pwsinvg  14935  pwssub  14936  galactghm  15111  efginvrel1  15365  frgpup3lem  15414  gsumzf1o  15524  gsumconst  15537  gsumzmhm  15538  gsummhm2  15540  gsumsub  15547  gsum2d  15551  dprdfsub  15584  lmhmvsca  16126  psrass1lem  16447  psrlinv  16466  psrcom  16477  evlslem2  16573  coe1fval3  16611  psropprmul  16637  coe1z  16661  coe1mul2  16667  coe1tm  16670  ply1coe  16689  frgpcyg  16859  ptrescn  17676  lmcn2  17686  qtopeu  17753  flfcnp2  18044  tgpconcomp  18147  tsmsmhm  18180  tsmssub  18183  tsmsxplem1  18187  negfcncf  18954  pcopt  19052  pcopt2  19053  pi1xfrcnvlem  19086  ovolctb  19391  ovolfs2  19468  uniioombllem2  19480  uniioombllem3  19482  ismbf  19525  mbfconst  19530  ismbfcn2  19534  itg1climres  19609  iblabslem  19722  iblabs  19723  bddmulibl  19733  limccnp  19783  limccnp2  19784  limcco  19785  dvcof  19839  dvcjbr  19840  dvcj  19841  dvfre  19842  dvmptcj  19859  dvmptco  19863  dvcnvlem  19865  dvef  19869  dvlip  19882  dvlipcn  19883  itgsubstlem  19937  plypf1  20136  plyco  20165  dgrcolem1  20196  dgrcolem2  20197  dgrco  20198  plycjlem  20199  taylply2  20289  logcn  20543  leibpi  20787  efrlim  20813  jensenlem2  20831  amgmlem  20833  ftalem7  20866  lgseisenlem4  21141  dchrisum0  21219  cofmpt  24083  ofcfval4  24493  dstfrvclim1  24740  lgamgulmlem2  24819  lgamcvg2  24844  cvmliftlem6  24982  cvmliftphtlem  25009  cvmlift3lem5  25015  circum  25116  mblfinlem2  26256  volsupnfl  26263  itgaddnc  26279  itgmulc2nc  26287  ftc1anclem1  26294  ftc1anclem2  26295  ftc1anclem3  26296  ftc1anclem4  26297  ftc1anclem5  26298  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anclem8  26301  fnopabco  26438  upixp  26445  mhmvlin  27443  mendassa  27493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-fv 5465
  Copyright terms: Public domain W3C validator