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

Theorem fmptco 6056
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 5333 . 2  |-  Rel  ( G  o.  F )
2 funmpt 5618 . . 3  |-  Fun  (
x  e.  A  |->  T )
3 funrel 5599 . . 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 2451 . . . . . . . . . . . . 13  |-  ( x  e.  A  |->  R )  =  ( x  e.  A  |->  R )
75, 6fmptd 6046 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  A  |->  R ) : A --> B )
8 fmptco.2 . . . . . . . . . . . . 13  |-  ( ph  ->  F  =  ( x  e.  A  |->  R ) )
98feq1d 5714 . . . . . . . . . . . 12  |-  ( ph  ->  ( F : A --> B 
<->  ( x  e.  A  |->  R ) : A --> B ) )
107, 9mpbird 236 . . . . . . . . . . 11  |-  ( ph  ->  F : A --> B )
11 ffun 5731 . . . . . . . . . . 11  |-  ( F : A --> B  ->  Fun  F )
1210, 11syl 17 . . . . . . . . . 10  |-  ( ph  ->  Fun  F )
13 funbrfv 5903 . . . . . . . . . . 11  |-  ( Fun 
F  ->  ( z F u  ->  ( F `
 z )  =  u ) )
1413imp 431 . . . . . . . . . 10  |-  ( ( Fun  F  /\  z F u )  -> 
( F `  z
)  =  u )
1512, 14sylan 474 . . . . . . . . 9  |-  ( (
ph  /\  z F u )  ->  ( F `  z )  =  u )
1615eqcomd 2457 . . . . . . . 8  |-  ( (
ph  /\  z F u )  ->  u  =  ( F `  z ) )
1716a1d 26 . . . . . . 7  |-  ( (
ph  /\  z F u )  ->  (
u G w  ->  u  =  ( F `  z ) ) )
1817expimpd 608 . . . . . 6  |-  ( ph  ->  ( ( z F u  /\  u G w )  ->  u  =  ( F `  z ) ) )
1918pm4.71rd 641 . . . . 5  |-  ( ph  ->  ( ( z F u  /\  u G w )  <->  ( u  =  ( F `  z )  /\  (
z F u  /\  u G w ) ) ) )
2019exbidv 1768 . . . 4  |-  ( ph  ->  ( E. u ( z F u  /\  u G w )  <->  E. u
( u  =  ( F `  z )  /\  ( z F u  /\  u G w ) ) ) )
21 fvex 5875 . . . . . 6  |-  ( F `
 z )  e. 
_V
22 breq2 4406 . . . . . . 7  |-  ( u  =  ( F `  z )  ->  (
z F u  <->  z F
( F `  z
) ) )
23 breq1 4405 . . . . . . 7  |-  ( u  =  ( F `  z )  ->  (
u G w  <->  ( F `  z ) G w ) )
2422, 23anbi12d 717 . . . . . 6  |-  ( u  =  ( F `  z )  ->  (
( z F u  /\  u G w )  <->  ( z F ( F `  z
)  /\  ( F `  z ) G w ) ) )
2521, 24ceqsexv 3084 . . . . 5  |-  ( E. u ( u  =  ( F `  z
)  /\  ( z F u  /\  u G w ) )  <-> 
( z F ( F `  z )  /\  ( F `  z ) G w ) )
26 funfvbrb 5995 . . . . . . . . 9  |-  ( Fun 
F  ->  ( z  e.  dom  F  <->  z F
( F `  z
) ) )
2712, 26syl 17 . . . . . . . 8  |-  ( ph  ->  ( z  e.  dom  F  <-> 
z F ( F `
 z ) ) )
28 fdm 5733 . . . . . . . . . 10  |-  ( F : A --> B  ->  dom  F  =  A )
2910, 28syl 17 . . . . . . . . 9  |-  ( ph  ->  dom  F  =  A )
3029eleq2d 2514 . . . . . . . 8  |-  ( ph  ->  ( z  e.  dom  F  <-> 
z  e.  A ) )
3127, 30bitr3d 259 . . . . . . 7  |-  ( ph  ->  ( z F ( F `  z )  <-> 
z  e.  A ) )
328fveq1d 5867 . . . . . . . 8  |-  ( ph  ->  ( F `  z
)  =  ( ( x  e.  A  |->  R ) `  z ) )
33 fmptco.3 . . . . . . . 8  |-  ( ph  ->  G  =  ( y  e.  B  |->  S ) )
34 eqidd 2452 . . . . . . . 8  |-  ( ph  ->  w  =  w )
3532, 33, 34breq123d 4416 . . . . . . 7  |-  ( ph  ->  ( ( F `  z ) G w  <-> 
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w ) )
3631, 35anbi12d 717 . . . . . 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 2592 . . . . . . . . 9  |-  F/_ x
z
38 nfv 1761 . . . . . . . . . 10  |-  F/ x ph
39 nffvmpt1 5873 . . . . . . . . . . . 12  |-  F/_ x
( ( x  e.  A  |->  R ) `  z )
40 nfcv 2592 . . . . . . . . . . . 12  |-  F/_ x
( y  e.  B  |->  S )
41 nfcv 2592 . . . . . . . . . . . 12  |-  F/_ x w
4239, 40, 41nfbr 4447 . . . . . . . . . . 11  |-  F/ x
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w
43 nfcsb1v 3379 . . . . . . . . . . . 12  |-  F/_ x [_ z  /  x ]_ T
4443nfeq2 2607 . . . . . . . . . . 11  |-  F/ x  w  =  [_ z  /  x ]_ T
4542, 44nfbi 2017 . . . . . . . . . 10  |-  F/ x
( ( ( x  e.  A  |->  R ) `
 z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T )
4638, 45nfim 2003 . . . . . . . . 9  |-  F/ x
( ph  ->  ( ( ( x  e.  A  |->  R ) `  z
) ( y  e.  B  |->  S ) w  <-> 
w  =  [_ z  /  x ]_ T ) )
47 fveq2 5865 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( x  e.  A  |->  R ) `  x
)  =  ( ( x  e.  A  |->  R ) `  z ) )
4847breq1d 4412 . . . . . . . . . . 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 3372 . . . . . . . . . . . 12  |-  ( x  =  z  ->  T  =  [_ z  /  x ]_ T )
5049eqeq2d 2461 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
w  =  T  <->  w  =  [_ z  /  x ]_ T ) )
5148, 50bibi12d 323 . . . . . . . . . 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 318 . . . . . . . . 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 3048 . . . . . . . . . . . 12  |-  w  e. 
_V
54 simpl 459 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  y  =  R )
5554eleq1d 2513 . . . . . . . . . . . . . 14  |-  ( ( y  =  R  /\  u  =  w )  ->  ( y  e.  B  <->  R  e.  B ) )
56 simpr 463 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  u  =  w )
57 fmptco.4 . . . . . . . . . . . . . . . 16  |-  ( y  =  R  ->  S  =  T )
5857adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  S  =  T )
5956, 58eqeq12d 2466 . . . . . . . . . . . . . 14  |-  ( ( y  =  R  /\  u  =  w )  ->  ( u  =  S  <-> 
w  =  T ) )
6055, 59anbi12d 717 . . . . . . . . . . . . 13  |-  ( ( y  =  R  /\  u  =  w )  ->  ( ( y  e.  B  /\  u  =  S )  <->  ( R  e.  B  /\  w  =  T ) ) )
61 df-mpt 4463 . . . . . . . . . . . . 13  |-  ( y  e.  B  |->  S )  =  { <. y ,  u >.  |  (
y  e.  B  /\  u  =  S ) }
6260, 61brabga 4715 . . . . . . . . . . . 12  |-  ( ( R  e.  B  /\  w  e.  _V )  ->  ( R ( y  e.  B  |->  S ) w  <->  ( R  e.  B  /\  w  =  T ) ) )
635, 53, 62sylancl 668 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ( R ( y  e.  B  |->  S ) w  <-> 
( R  e.  B  /\  w  =  T
) ) )
64 simpr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
656fvmpt2 5957 . . . . . . . . . . . . 13  |-  ( ( x  e.  A  /\  R  e.  B )  ->  ( ( x  e.  A  |->  R ) `  x )  =  R )
6664, 5, 65syl2anc 667 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  R ) `  x
)  =  R )
6766breq1d 4412 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  R ( y  e.  B  |->  S ) w ) )
685biantrurd 511 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
w  =  T  <->  ( R  e.  B  /\  w  =  T ) ) )
6963, 67, 683bitr4d 289 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  w  =  T
) )
7069expcom 437 . . . . . . . . 9  |-  ( x  e.  A  ->  ( ph  ->  ( ( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  w  =  T ) ) )
7137, 46, 52, 70vtoclgaf 3112 . . . . . . . 8  |-  ( z  e.  A  ->  ( ph  ->  ( ( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T ) ) )
7271impcom 432 . . . . . . 7  |-  ( (
ph  /\  z  e.  A )  ->  (
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T ) )
7372pm5.32da 647 . . . . . 6  |-  ( ph  ->  ( ( z  e.  A  /\  ( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w )  <-> 
( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
7436, 73bitrd 257 . . . . 5  |-  ( ph  ->  ( ( z F ( F `  z
)  /\  ( F `  z ) G w )  <->  ( z  e.  A  /\  w  = 
[_ z  /  x ]_ T ) ) )
7525, 74syl5bb 261 . . . 4  |-  ( ph  ->  ( E. u ( u  =  ( F `
 z )  /\  ( z F u  /\  u G w ) )  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
7620, 75bitrd 257 . . 3  |-  ( ph  ->  ( E. u ( z F u  /\  u G w )  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
77 vex 3048 . . . 4  |-  z  e. 
_V
7877, 53opelco 5006 . . 3  |-  ( <.
z ,  w >.  e.  ( G  o.  F
)  <->  E. u ( z F u  /\  u G w ) )
79 df-mpt 4463 . . . . 5  |-  ( x  e.  A  |->  T )  =  { <. x ,  v >.  |  ( x  e.  A  /\  v  =  T ) }
8079eleq2i 2521 . . . 4  |-  ( <.
z ,  w >.  e.  ( x  e.  A  |->  T )  <->  <. z ,  w >.  e.  { <. x ,  v >.  |  ( x  e.  A  /\  v  =  T ) } )
81 nfv 1761 . . . . . 6  |-  F/ x  z  e.  A
8243nfeq2 2607 . . . . . 6  |-  F/ x  v  =  [_ z  /  x ]_ T
8381, 82nfan 2011 . . . . 5  |-  F/ x
( z  e.  A  /\  v  =  [_ z  /  x ]_ T )
84 nfv 1761 . . . . 5  |-  F/ v ( z  e.  A  /\  w  =  [_ z  /  x ]_ T )
85 eleq1 2517 . . . . . 6  |-  ( x  =  z  ->  (
x  e.  A  <->  z  e.  A ) )
8649eqeq2d 2461 . . . . . 6  |-  ( x  =  z  ->  (
v  =  T  <->  v  =  [_ z  /  x ]_ T ) )
8785, 86anbi12d 717 . . . . 5  |-  ( x  =  z  ->  (
( x  e.  A  /\  v  =  T
)  <->  ( z  e.  A  /\  v  = 
[_ z  /  x ]_ T ) ) )
88 eqeq1 2455 . . . . . 6  |-  ( v  =  w  ->  (
v  =  [_ z  /  x ]_ T  <->  w  =  [_ z  /  x ]_ T ) )
8988anbi2d 710 . . . . 5  |-  ( v  =  w  ->  (
( z  e.  A  /\  v  =  [_ z  /  x ]_ T )  <-> 
( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
9083, 84, 77, 53, 87, 89opelopabf 4726 . . . 4  |-  ( <.
z ,  w >.  e. 
{ <. x ,  v
>.  |  ( x  e.  A  /\  v  =  T ) }  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) )
9180, 90bitri 253 . . 3  |-  ( <.
z ,  w >.  e.  ( x  e.  A  |->  T )  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) )
9276, 78, 913bitr4g 292 . 2  |-  ( ph  ->  ( <. z ,  w >.  e.  ( G  o.  F )  <->  <. z ,  w >.  e.  (
x  e.  A  |->  T ) ) )
931, 4, 92eqrelrdv 4931 1  |-  ( ph  ->  ( G  o.  F
)  =  ( x  e.  A  |->  T ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1444   E.wex 1663    e. wcel 1887   _Vcvv 3045   [_csb 3363   <.cop 3974   class class class wbr 4402   {copab 4460    |-> cmpt 4461   dom cdm 4834    o. ccom 4838   Rel wrel 4839   Fun wfun 5576   -->wf 5578   ` cfv 5582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-fv 5590
This theorem is referenced by:  fmptcof  6057  fcompt  6059  fcoconst  6060  ofco  6551  ccatco  12932  lo1o12  13597  rlimcn1  13652  rlimcn1b  13653  rlimdiv  13709  ackbijnn  13886  setcepi  15983  prf1st  16089  prf2nd  16090  hofcllem  16143  prdsidlem  16568  pws0g  16572  pwsco1mhm  16617  pwsco2mhm  16618  pwsinvg  16798  pwssub  16799  galactghm  17044  efginvrel1  17378  frgpup3lem  17427  gsumzf1o  17546  gsumconst  17567  gsummptshft  17569  gsumzmhm  17570  gsummhm2  17572  gsummptmhm  17573  gsumsub  17581  gsum2dlem2  17603  dprdfsub  17654  lmhmvsca  18268  psrass1lem  18601  psrlinv  18621  psrcom  18633  evlslem2  18735  coe1fval3  18801  psropprmul  18831  coe1z  18856  coe1mul2  18862  coe1tm  18866  ply1coe  18889  ply1coeOLD  18890  evls1sca  18912  frgpcyg  19144  evpmodpmf1o  19164  mhmvlin  19422  ofco2  19476  mdetleib2  19613  mdetralt  19633  smadiadetlem3  19693  ptrescn  20654  lmcn2  20664  qtopeu  20731  flfcnp2  21022  tgpconcomp  21127  tsmsmhm  21160  tsmssub  21163  tsmsxplem1  21167  negfcncf  21951  pcopt  22053  pcopt2  22054  pi1xfrcnvlem  22087  ovolctb  22443  ovolfs2  22523  uniioombllem2  22540  uniioombllem2OLD  22541  uniioombllem3  22543  ismbf  22586  mbfconst  22591  ismbfcn2  22595  itg1climres  22672  iblabslem  22785  iblabs  22786  bddmulibl  22796  limccnp  22846  limccnp2  22847  limcco  22848  dvcof  22902  dvcjbr  22903  dvcj  22904  dvfre  22905  dvmptcj  22922  dvmptco  22926  dvcnvlem  22928  dvef  22932  dvlip  22945  dvlipcn  22946  itgsubstlem  23000  plypf1  23166  plyco  23195  dgrcolem1  23227  dgrcolem2  23228  dgrco  23229  plycjlem  23230  taylply2  23323  logcn  23592  leibpi  23868  efrlim  23895  jensenlem2  23913  amgmlem  23915  lgamgulmlem2  23955  lgamcvg2  23980  ftalem7  24005  lgseisenlem4  24280  dchrisum0  24358  cofmpt  28266  ofcfval4  28926  eulerpartgbij  29205  dstfrvclim1  29310  cvmliftlem6  30013  cvmliftphtlem  30040  cvmlift3lem5  30046  elmsubrn  30166  msubco  30169  circum  30318  mblfinlem2  31978  volsupnfl  31985  itgaddnc  32002  itgmulc2nc  32010  ftc1anclem1  32017  ftc1anclem2  32018  ftc1anclem3  32019  ftc1anclem4  32020  ftc1anclem5  32021  ftc1anclem6  32022  ftc1anclem7  32023  ftc1anclem8  32024  fnopabco  32049  upixp  32056  mendassa  36060  cncfcompt  37760  dvcosax  37798  dirkercncflem4  37968  fourierdlem111  38081  meadjiunlem  38303  meadjiun  38304
  Copyright terms: Public domain W3C validator