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

Theorem fmptco 5691
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 5171 . 2  |-  Rel  ( G  o.  F )
2 funmpt 5290 . . 3  |-  Fun  (
x  e.  A  |->  T )
3 funrel 5272 . . 3  |-  ( Fun  ( x  e.  A  |->  T )  ->  Rel  ( x  e.  A  |->  T ) )
42, 3ax-mp 8 . 2  |-  Rel  (
x  e.  A  |->  T )
5 fmptco.1 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  R  e.  B )
6 eqid 2283 . . . . . . . . . . . . 13  |-  ( x  e.  A  |->  R )  =  ( x  e.  A  |->  R )
75, 6fmptd 5684 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  A  |->  R ) : A --> B )
8 fmptco.2 . . . . . . . . . . . . 13  |-  ( ph  ->  F  =  ( x  e.  A  |->  R ) )
98feq1d 5379 . . . . . . . . . . . 12  |-  ( ph  ->  ( F : A --> B 
<->  ( x  e.  A  |->  R ) : A --> B ) )
107, 9mpbird 223 . . . . . . . . . . 11  |-  ( ph  ->  F : A --> B )
11 ffun 5391 . . . . . . . . . . 11  |-  ( F : A --> B  ->  Fun  F )
1210, 11syl 15 . . . . . . . . . 10  |-  ( ph  ->  Fun  F )
13 funbrfv 5561 . . . . . . . . . . 11  |-  ( Fun 
F  ->  ( z F u  ->  ( F `
 z )  =  u ) )
1413imp 418 . . . . . . . . . 10  |-  ( ( Fun  F  /\  z F u )  -> 
( F `  z
)  =  u )
1512, 14sylan 457 . . . . . . . . 9  |-  ( (
ph  /\  z F u )  ->  ( F `  z )  =  u )
1615eqcomd 2288 . . . . . . . 8  |-  ( (
ph  /\  z F u )  ->  u  =  ( F `  z ) )
1716a1d 22 . . . . . . 7  |-  ( (
ph  /\  z F u )  ->  (
u G w  ->  u  =  ( F `  z ) ) )
1817expimpd 586 . . . . . 6  |-  ( ph  ->  ( ( z F u  /\  u G w )  ->  u  =  ( F `  z ) ) )
1918pm4.71rd 616 . . . . 5  |-  ( ph  ->  ( ( z F u  /\  u G w )  <->  ( u  =  ( F `  z )  /\  (
z F u  /\  u G w ) ) ) )
2019exbidv 1612 . . . 4  |-  ( ph  ->  ( E. u ( z F u  /\  u G w )  <->  E. u
( u  =  ( F `  z )  /\  ( z F u  /\  u G w ) ) ) )
21 fvex 5539 . . . . . 6  |-  ( F `
 z )  e. 
_V
22 breq2 4027 . . . . . . 7  |-  ( u  =  ( F `  z )  ->  (
z F u  <->  z F
( F `  z
) ) )
23 breq1 4026 . . . . . . 7  |-  ( u  =  ( F `  z )  ->  (
u G w  <->  ( F `  z ) G w ) )
2422, 23anbi12d 691 . . . . . 6  |-  ( u  =  ( F `  z )  ->  (
( z F u  /\  u G w )  <->  ( z F ( F `  z
)  /\  ( F `  z ) G w ) ) )
2521, 24ceqsexv 2823 . . . . 5  |-  ( E. u ( u  =  ( F `  z
)  /\  ( z F u  /\  u G w ) )  <-> 
( z F ( F `  z )  /\  ( F `  z ) G w ) )
26 funfvbrb 5638 . . . . . . . . 9  |-  ( Fun 
F  ->  ( z  e.  dom  F  <->  z F
( F `  z
) ) )
2712, 26syl 15 . . . . . . . 8  |-  ( ph  ->  ( z  e.  dom  F  <-> 
z F ( F `
 z ) ) )
28 fdm 5393 . . . . . . . . . 10  |-  ( F : A --> B  ->  dom  F  =  A )
2910, 28syl 15 . . . . . . . . 9  |-  ( ph  ->  dom  F  =  A )
3029eleq2d 2350 . . . . . . . 8  |-  ( ph  ->  ( z  e.  dom  F  <-> 
z  e.  A ) )
3127, 30bitr3d 246 . . . . . . 7  |-  ( ph  ->  ( z F ( F `  z )  <-> 
z  e.  A ) )
328fveq1d 5527 . . . . . . . 8  |-  ( ph  ->  ( F `  z
)  =  ( ( x  e.  A  |->  R ) `  z ) )
33 fmptco.3 . . . . . . . 8  |-  ( ph  ->  G  =  ( y  e.  B  |->  S ) )
34 eqidd 2284 . . . . . . . 8  |-  ( ph  ->  w  =  w )
3532, 33, 34breq123d 4037 . . . . . . 7  |-  ( ph  ->  ( ( F `  z ) G w  <-> 
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w ) )
3631, 35anbi12d 691 . . . . . 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 2419 . . . . . . . . 9  |-  F/_ x
z
38 nfv 1605 . . . . . . . . . 10  |-  F/ x ph
39 nfmpt1 4109 . . . . . . . . . . . . 13  |-  F/_ x
( x  e.  A  |->  R )
4039, 37nffv 5532 . . . . . . . . . . . 12  |-  F/_ x
( ( x  e.  A  |->  R ) `  z )
41 nfcv 2419 . . . . . . . . . . . 12  |-  F/_ x
( y  e.  B  |->  S )
42 nfcv 2419 . . . . . . . . . . . 12  |-  F/_ x w
4340, 41, 42nfbr 4067 . . . . . . . . . . 11  |-  F/ x
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w
44 nfcsb1v 3113 . . . . . . . . . . . 12  |-  F/_ x [_ z  /  x ]_ T
4544nfeq2 2430 . . . . . . . . . . 11  |-  F/ x  w  =  [_ z  /  x ]_ T
4643, 45nfbi 1772 . . . . . . . . . 10  |-  F/ x
( ( ( x  e.  A  |->  R ) `
 z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T )
4738, 46nfim 1769 . . . . . . . . 9  |-  F/ x
( ph  ->  ( ( ( x  e.  A  |->  R ) `  z
) ( y  e.  B  |->  S ) w  <-> 
w  =  [_ z  /  x ]_ T ) )
48 fveq2 5525 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( x  e.  A  |->  R ) `  x
)  =  ( ( x  e.  A  |->  R ) `  z ) )
4948breq1d 4033 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  ( ( x  e.  A  |->  R ) `
 z ) ( y  e.  B  |->  S ) w ) )
50 csbeq1a 3089 . . . . . . . . . . . 12  |-  ( x  =  z  ->  T  =  [_ z  /  x ]_ T )
5150eqeq2d 2294 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
w  =  T  <->  w  =  [_ z  /  x ]_ T ) )
5249, 51bibi12d 312 . . . . . . . . . 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 ) ) )
5352imbi2d 307 . . . . . . . . 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 ) ) ) )
54 vex 2791 . . . . . . . . . . . 12  |-  w  e. 
_V
55 simpl 443 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  y  =  R )
5655eleq1d 2349 . . . . . . . . . . . . . 14  |-  ( ( y  =  R  /\  u  =  w )  ->  ( y  e.  B  <->  R  e.  B ) )
57 simpr 447 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  u  =  w )
58 fmptco.4 . . . . . . . . . . . . . . . 16  |-  ( y  =  R  ->  S  =  T )
5958adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  S  =  T )
6057, 59eqeq12d 2297 . . . . . . . . . . . . . 14  |-  ( ( y  =  R  /\  u  =  w )  ->  ( u  =  S  <-> 
w  =  T ) )
6156, 60anbi12d 691 . . . . . . . . . . . . 13  |-  ( ( y  =  R  /\  u  =  w )  ->  ( ( y  e.  B  /\  u  =  S )  <->  ( R  e.  B  /\  w  =  T ) ) )
62 df-mpt 4079 . . . . . . . . . . . . 13  |-  ( y  e.  B  |->  S )  =  { <. y ,  u >.  |  (
y  e.  B  /\  u  =  S ) }
6361, 62brabga 4279 . . . . . . . . . . . 12  |-  ( ( R  e.  B  /\  w  e.  _V )  ->  ( R ( y  e.  B  |->  S ) w  <->  ( R  e.  B  /\  w  =  T ) ) )
645, 54, 63sylancl 643 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ( R ( y  e.  B  |->  S ) w  <-> 
( R  e.  B  /\  w  =  T
) ) )
65 simpr 447 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
666fvmpt2 5608 . . . . . . . . . . . . 13  |-  ( ( x  e.  A  /\  R  e.  B )  ->  ( ( x  e.  A  |->  R ) `  x )  =  R )
6765, 5, 66syl2anc 642 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  R ) `  x
)  =  R )
6867breq1d 4033 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  R ( y  e.  B  |->  S ) w ) )
695biantrurd 494 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
w  =  T  <->  ( R  e.  B  /\  w  =  T ) ) )
7064, 68, 693bitr4d 276 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  w  =  T
) )
7170expcom 424 . . . . . . . . 9  |-  ( x  e.  A  ->  ( ph  ->  ( ( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  w  =  T ) ) )
7237, 47, 53, 71vtoclgaf 2848 . . . . . . . 8  |-  ( z  e.  A  ->  ( ph  ->  ( ( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T ) ) )
7372impcom 419 . . . . . . 7  |-  ( (
ph  /\  z  e.  A )  ->  (
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T ) )
7473pm5.32da 622 . . . . . 6  |-  ( ph  ->  ( ( z  e.  A  /\  ( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w )  <-> 
( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
7536, 74bitrd 244 . . . . 5  |-  ( ph  ->  ( ( z F ( F `  z
)  /\  ( F `  z ) G w )  <->  ( z  e.  A  /\  w  = 
[_ z  /  x ]_ T ) ) )
7625, 75syl5bb 248 . . . 4  |-  ( ph  ->  ( E. u ( u  =  ( F `
 z )  /\  ( z F u  /\  u G w ) )  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
7720, 76bitrd 244 . . 3  |-  ( ph  ->  ( E. u ( z F u  /\  u G w )  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
78 vex 2791 . . . 4  |-  z  e. 
_V
7978, 54opelco 4853 . . 3  |-  ( <.
z ,  w >.  e.  ( G  o.  F
)  <->  E. u ( z F u  /\  u G w ) )
80 df-mpt 4079 . . . . 5  |-  ( x  e.  A  |->  T )  =  { <. x ,  v >.  |  ( x  e.  A  /\  v  =  T ) }
8180eleq2i 2347 . . . 4  |-  ( <.
z ,  w >.  e.  ( x  e.  A  |->  T )  <->  <. z ,  w >.  e.  { <. x ,  v >.  |  ( x  e.  A  /\  v  =  T ) } )
82 nfv 1605 . . . . . 6  |-  F/ x  z  e.  A
8344nfeq2 2430 . . . . . 6  |-  F/ x  v  =  [_ z  /  x ]_ T
8482, 83nfan 1771 . . . . 5  |-  F/ x
( z  e.  A  /\  v  =  [_ z  /  x ]_ T )
85 nfv 1605 . . . . 5  |-  F/ v ( z  e.  A  /\  w  =  [_ z  /  x ]_ T )
86 eleq1 2343 . . . . . 6  |-  ( x  =  z  ->  (
x  e.  A  <->  z  e.  A ) )
8750eqeq2d 2294 . . . . . 6  |-  ( x  =  z  ->  (
v  =  T  <->  v  =  [_ z  /  x ]_ T ) )
8886, 87anbi12d 691 . . . . 5  |-  ( x  =  z  ->  (
( x  e.  A  /\  v  =  T
)  <->  ( z  e.  A  /\  v  = 
[_ z  /  x ]_ T ) ) )
89 eqeq1 2289 . . . . . 6  |-  ( v  =  w  ->  (
v  =  [_ z  /  x ]_ T  <->  w  =  [_ z  /  x ]_ T ) )
9089anbi2d 684 . . . . 5  |-  ( v  =  w  ->  (
( z  e.  A  /\  v  =  [_ z  /  x ]_ T )  <-> 
( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
9184, 85, 78, 54, 88, 90opelopabf 4289 . . . 4  |-  ( <.
z ,  w >.  e. 
{ <. x ,  v
>.  |  ( x  e.  A  /\  v  =  T ) }  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) )
9281, 91bitri 240 . . 3  |-  ( <.
z ,  w >.  e.  ( x  e.  A  |->  T )  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) )
9377, 79, 923bitr4g 279 . 2  |-  ( ph  ->  ( <. z ,  w >.  e.  ( G  o.  F )  <->  <. z ,  w >.  e.  (
x  e.  A  |->  T ) ) )
941, 4, 93eqrelrdv 4783 1  |-  ( ph  ->  ( G  o.  F
)  =  ( x  e.  A  |->  T ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   E.wex 1528    = wceq 1623    e. wcel 1684   _Vcvv 2788   [_csb 3081   <.cop 3643   class class class wbr 4023   {copab 4076    e. cmpt 4077   dom cdm 4689    o. ccom 4693   Rel wrel 4694   Fun wfun 5249   -->wf 5251   ` cfv 5255
This theorem is referenced by:  fmptcof  5692  fcompt  5694  fcoconst  5695  ofco  6097  ccatco  11490  lo1o12  12007  rlimcn1  12062  rlimcn1b  12063  rlimdiv  12119  ackbijnn  12286  setcepi  13920  prf1st  13978  prf2nd  13979  hofcllem  14032  yonedalem3b  14053  prdsidlem  14404  pws0g  14408  pwsco1mhm  14446  pwsco2mhm  14447  pwsinvg  14607  pwssub  14608  galactghm  14783  efginvrel1  15037  frgpup3lem  15086  gsumzf1o  15196  gsumconst  15209  gsumzmhm  15210  gsummhm2  15212  gsumsub  15219  gsum2d  15223  dprdfsub  15256  lmhmvsca  15802  psrass1lem  16123  psrlinv  16142  psrcom  16153  evlslem2  16249  coe1fval3  16289  psropprmul  16316  coe1z  16340  coe1mul2  16346  coe1tm  16349  ply1coe  16368  frgpcyg  16527  ptrescn  17333  lmcn2  17343  qtopeu  17407  flfcnp2  17702  tgpconcomp  17795  tsmsmhm  17828  tsmssub  17831  tsmsxplem1  17835  negfcncf  18422  pcopt  18520  pcopt2  18521  pi1xfrcnvlem  18554  ovolctb  18849  ovolfs2  18926  uniioombllem2  18938  uniioombllem3  18940  ismbf  18985  mbfconst  18990  ismbfcn2  18994  itg1climres  19069  iblabslem  19182  iblabs  19183  bddmulibl  19193  limccnp  19241  limccnp2  19242  limcco  19243  dvcof  19297  dvcjbr  19298  dvcj  19299  dvfre  19300  dvmptcj  19317  dvmptco  19321  dvcnvlem  19323  dvef  19327  dvlip  19340  dvlipcn  19341  itgsubstlem  19395  plypf1  19594  plyco  19623  dgrcolem1  19654  dgrcolem2  19655  dgrco  19656  plycjlem  19657  taylply2  19747  logcn  19994  leibpi  20238  efrlim  20264  jensenlem2  20282  amgmlem  20284  ftalem7  20316  lgseisenlem4  20591  dchrisum0  20669  cofmpt  23231  ofcfval4  23466  dstfrvclim1  23678  cvmliftlem6  23821  cvmliftphtlem  23848  cvmlift3lem5  23854  circum  24007  cmprtr  25396  ltrcmp  25405  cmpltr2  25407  cmperltr  25409  cmprltr  25410  fnopabco  26388  upixp  26403  mhmvlin  27452  mendassa  27502
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263
  Copyright terms: Public domain W3C validator