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

Theorem fmptco 5707
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 5187 . 2  |-  Rel  ( G  o.  F )
2 funmpt 5306 . . 3  |-  Fun  (
x  e.  A  |->  T )
3 funrel 5288 . . 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 2296 . . . . . . . . . . . . 13  |-  ( x  e.  A  |->  R )  =  ( x  e.  A  |->  R )
75, 6fmptd 5700 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  A  |->  R ) : A --> B )
8 fmptco.2 . . . . . . . . . . . . 13  |-  ( ph  ->  F  =  ( x  e.  A  |->  R ) )
98feq1d 5395 . . . . . . . . . . . 12  |-  ( ph  ->  ( F : A --> B 
<->  ( x  e.  A  |->  R ) : A --> B ) )
107, 9mpbird 223 . . . . . . . . . . 11  |-  ( ph  ->  F : A --> B )
11 ffun 5407 . . . . . . . . . . 11  |-  ( F : A --> B  ->  Fun  F )
1210, 11syl 15 . . . . . . . . . 10  |-  ( ph  ->  Fun  F )
13 funbrfv 5577 . . . . . . . . . . 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 2301 . . . . . . . 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 1616 . . . 4  |-  ( ph  ->  ( E. u ( z F u  /\  u G w )  <->  E. u
( u  =  ( F `  z )  /\  ( z F u  /\  u G w ) ) ) )
21 fvex 5555 . . . . . 6  |-  ( F `
 z )  e. 
_V
22 breq2 4043 . . . . . . 7  |-  ( u  =  ( F `  z )  ->  (
z F u  <->  z F
( F `  z
) ) )
23 breq1 4042 . . . . . . 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 2836 . . . . 5  |-  ( E. u ( u  =  ( F `  z
)  /\  ( z F u  /\  u G w ) )  <-> 
( z F ( F `  z )  /\  ( F `  z ) G w ) )
26 funfvbrb 5654 . . . . . . . . 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 5409 . . . . . . . . . 10  |-  ( F : A --> B  ->  dom  F  =  A )
2910, 28syl 15 . . . . . . . . 9  |-  ( ph  ->  dom  F  =  A )
3029eleq2d 2363 . . . . . . . 8  |-  ( ph  ->  ( z  e.  dom  F  <-> 
z  e.  A ) )
3127, 30bitr3d 246 . . . . . . 7  |-  ( ph  ->  ( z F ( F `  z )  <-> 
z  e.  A ) )
328fveq1d 5543 . . . . . . . 8  |-  ( ph  ->  ( F `  z
)  =  ( ( x  e.  A  |->  R ) `  z ) )
33 fmptco.3 . . . . . . . 8  |-  ( ph  ->  G  =  ( y  e.  B  |->  S ) )
34 eqidd 2297 . . . . . . . 8  |-  ( ph  ->  w  =  w )
3532, 33, 34breq123d 4053 . . . . . . 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 2432 . . . . . . . . 9  |-  F/_ x
z
38 nfv 1609 . . . . . . . . . 10  |-  F/ x ph
39 nfmpt1 4125 . . . . . . . . . . . . 13  |-  F/_ x
( x  e.  A  |->  R )
4039, 37nffv 5548 . . . . . . . . . . . 12  |-  F/_ x
( ( x  e.  A  |->  R ) `  z )
41 nfcv 2432 . . . . . . . . . . . 12  |-  F/_ x
( y  e.  B  |->  S )
42 nfcv 2432 . . . . . . . . . . . 12  |-  F/_ x w
4340, 41, 42nfbr 4083 . . . . . . . . . . 11  |-  F/ x
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w
44 nfcsb1v 3126 . . . . . . . . . . . 12  |-  F/_ x [_ z  /  x ]_ T
4544nfeq2 2443 . . . . . . . . . . 11  |-  F/ x  w  =  [_ z  /  x ]_ T
4643, 45nfbi 1784 . . . . . . . . . 10  |-  F/ x
( ( ( x  e.  A  |->  R ) `
 z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T )
4738, 46nfim 1781 . . . . . . . . 9  |-  F/ x
( ph  ->  ( ( ( x  e.  A  |->  R ) `  z
) ( y  e.  B  |->  S ) w  <-> 
w  =  [_ z  /  x ]_ T ) )
48 fveq2 5541 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( x  e.  A  |->  R ) `  x
)  =  ( ( x  e.  A  |->  R ) `  z ) )
4948breq1d 4049 . . . . . . . . . . 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 3102 . . . . . . . . . . . 12  |-  ( x  =  z  ->  T  =  [_ z  /  x ]_ T )
5150eqeq2d 2307 . . . . . . . . . . 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 2804 . . . . . . . . . . . 12  |-  w  e. 
_V
55 simpl 443 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  y  =  R )
5655eleq1d 2362 . . . . . . . . . . . . . 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 2310 . . . . . . . . . . . . . 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 4095 . . . . . . . . . . . . 13  |-  ( y  e.  B  |->  S )  =  { <. y ,  u >.  |  (
y  e.  B  /\  u  =  S ) }
6361, 62brabga 4295 . . . . . . . . . . . 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 5624 . . . . . . . . . . . . 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 4049 . . . . . . . . . . 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 2861 . . . . . . . 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 2804 . . . 4  |-  z  e. 
_V
7978, 54opelco 4869 . . 3  |-  ( <.
z ,  w >.  e.  ( G  o.  F
)  <->  E. u ( z F u  /\  u G w ) )
80 df-mpt 4095 . . . . 5  |-  ( x  e.  A  |->  T )  =  { <. x ,  v >.  |  ( x  e.  A  /\  v  =  T ) }
8180eleq2i 2360 . . . 4  |-  ( <.
z ,  w >.  e.  ( x  e.  A  |->  T )  <->  <. z ,  w >.  e.  { <. x ,  v >.  |  ( x  e.  A  /\  v  =  T ) } )
82 nfv 1609 . . . . . 6  |-  F/ x  z  e.  A
8344nfeq2 2443 . . . . . 6  |-  F/ x  v  =  [_ z  /  x ]_ T
8482, 83nfan 1783 . . . . 5  |-  F/ x
( z  e.  A  /\  v  =  [_ z  /  x ]_ T )
85 nfv 1609 . . . . 5  |-  F/ v ( z  e.  A  /\  w  =  [_ z  /  x ]_ T )
86 eleq1 2356 . . . . . 6  |-  ( x  =  z  ->  (
x  e.  A  <->  z  e.  A ) )
8750eqeq2d 2307 . . . . . 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 2302 . . . . . 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 4305 . . . 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 4799 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 1531    = wceq 1632    e. wcel 1696   _Vcvv 2801   [_csb 3094   <.cop 3656   class class class wbr 4039   {copab 4092    e. cmpt 4093   dom cdm 4705    o. ccom 4709   Rel wrel 4710   Fun wfun 5265   -->wf 5267   ` cfv 5271
This theorem is referenced by:  fmptcof  5708  fcompt  5710  fcoconst  5711  ofco  6113  ccatco  11506  lo1o12  12023  rlimcn1  12078  rlimcn1b  12079  rlimdiv  12135  ackbijnn  12302  setcepi  13936  prf1st  13994  prf2nd  13995  hofcllem  14048  yonedalem3b  14069  prdsidlem  14420  pws0g  14424  pwsco1mhm  14462  pwsco2mhm  14463  pwsinvg  14623  pwssub  14624  galactghm  14799  efginvrel1  15053  frgpup3lem  15102  gsumzf1o  15212  gsumconst  15225  gsumzmhm  15226  gsummhm2  15228  gsumsub  15235  gsum2d  15239  dprdfsub  15272  lmhmvsca  15818  psrass1lem  16139  psrlinv  16158  psrcom  16169  evlslem2  16265  coe1fval3  16305  psropprmul  16332  coe1z  16356  coe1mul2  16362  coe1tm  16365  ply1coe  16384  frgpcyg  16543  ptrescn  17349  lmcn2  17359  qtopeu  17423  flfcnp2  17718  tgpconcomp  17811  tsmsmhm  17844  tsmssub  17847  tsmsxplem1  17851  negfcncf  18438  pcopt  18536  pcopt2  18537  pi1xfrcnvlem  18570  ovolctb  18865  ovolfs2  18942  uniioombllem2  18954  uniioombllem3  18956  ismbf  19001  mbfconst  19006  ismbfcn2  19010  itg1climres  19085  iblabslem  19198  iblabs  19199  bddmulibl  19209  limccnp  19257  limccnp2  19258  limcco  19259  dvcof  19313  dvcjbr  19314  dvcj  19315  dvfre  19316  dvmptcj  19333  dvmptco  19337  dvcnvlem  19339  dvef  19343  dvlip  19356  dvlipcn  19357  itgsubstlem  19411  plypf1  19610  plyco  19639  dgrcolem1  19670  dgrcolem2  19671  dgrco  19672  plycjlem  19673  taylply2  19763  logcn  20010  leibpi  20254  efrlim  20280  jensenlem2  20298  amgmlem  20300  ftalem7  20332  lgseisenlem4  20607  dchrisum0  20685  cofmpt  23246  ofcfval4  23481  dstfrvclim1  23693  cvmliftlem6  23836  cvmliftphtlem  23863  cvmlift3lem5  23869  circum  24022  itgaddnc  25011  itgmulc2nc  25019  cmprtr  25499  ltrcmp  25508  cmpltr2  25510  cmperltr  25512  cmprltr  25513  fnopabco  26491  upixp  26506  mhmvlin  27555  mendassa  27605
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-fv 5279
  Copyright terms: Public domain W3C validator