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

Theorem fmptco 5863
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 5324 . 2  |-  Rel  ( G  o.  F )
2 funmpt 5442 . . 3  |-  Fun  (
x  e.  A  |->  T )
3 funrel 5423 . . 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 2433 . . . . . . . . . . . . 13  |-  ( x  e.  A  |->  R )  =  ( x  e.  A  |->  R )
75, 6fmptd 5855 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  A  |->  R ) : A --> B )
8 fmptco.2 . . . . . . . . . . . . 13  |-  ( ph  ->  F  =  ( x  e.  A  |->  R ) )
98feq1d 5534 . . . . . . . . . . . 12  |-  ( ph  ->  ( F : A --> B 
<->  ( x  e.  A  |->  R ) : A --> B ) )
107, 9mpbird 232 . . . . . . . . . . 11  |-  ( ph  ->  F : A --> B )
11 ffun 5549 . . . . . . . . . . 11  |-  ( F : A --> B  ->  Fun  F )
1210, 11syl 16 . . . . . . . . . 10  |-  ( ph  ->  Fun  F )
13 funbrfv 5718 . . . . . . . . . . 11  |-  ( Fun 
F  ->  ( z F u  ->  ( F `
 z )  =  u ) )
1413imp 429 . . . . . . . . . 10  |-  ( ( Fun  F  /\  z F u )  -> 
( F `  z
)  =  u )
1512, 14sylan 468 . . . . . . . . 9  |-  ( (
ph  /\  z F u )  ->  ( F `  z )  =  u )
1615eqcomd 2438 . . . . . . . 8  |-  ( (
ph  /\  z F u )  ->  u  =  ( F `  z ) )
1716a1d 25 . . . . . . 7  |-  ( (
ph  /\  z F u )  ->  (
u G w  ->  u  =  ( F `  z ) ) )
1817expimpd 598 . . . . . 6  |-  ( ph  ->  ( ( z F u  /\  u G w )  ->  u  =  ( F `  z ) ) )
1918pm4.71rd 628 . . . . 5  |-  ( ph  ->  ( ( z F u  /\  u G w )  <->  ( u  =  ( F `  z )  /\  (
z F u  /\  u G w ) ) ) )
2019exbidv 1679 . . . 4  |-  ( ph  ->  ( E. u ( z F u  /\  u G w )  <->  E. u
( u  =  ( F `  z )  /\  ( z F u  /\  u G w ) ) ) )
21 fvex 5689 . . . . . 6  |-  ( F `
 z )  e. 
_V
22 breq2 4284 . . . . . . 7  |-  ( u  =  ( F `  z )  ->  (
z F u  <->  z F
( F `  z
) ) )
23 breq1 4283 . . . . . . 7  |-  ( u  =  ( F `  z )  ->  (
u G w  <->  ( F `  z ) G w ) )
2422, 23anbi12d 703 . . . . . 6  |-  ( u  =  ( F `  z )  ->  (
( z F u  /\  u G w )  <->  ( z F ( F `  z
)  /\  ( F `  z ) G w ) ) )
2521, 24ceqsexv 2998 . . . . 5  |-  ( E. u ( u  =  ( F `  z
)  /\  ( z F u  /\  u G w ) )  <-> 
( z F ( F `  z )  /\  ( F `  z ) G w ) )
26 funfvbrb 5804 . . . . . . . . 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 5551 . . . . . . . . . 10  |-  ( F : A --> B  ->  dom  F  =  A )
2910, 28syl 16 . . . . . . . . 9  |-  ( ph  ->  dom  F  =  A )
3029eleq2d 2500 . . . . . . . 8  |-  ( ph  ->  ( z  e.  dom  F  <-> 
z  e.  A ) )
3127, 30bitr3d 255 . . . . . . 7  |-  ( ph  ->  ( z F ( F `  z )  <-> 
z  e.  A ) )
328fveq1d 5681 . . . . . . . 8  |-  ( ph  ->  ( F `  z
)  =  ( ( x  e.  A  |->  R ) `  z ) )
33 fmptco.3 . . . . . . . 8  |-  ( ph  ->  G  =  ( y  e.  B  |->  S ) )
34 eqidd 2434 . . . . . . . 8  |-  ( ph  ->  w  =  w )
3532, 33, 34breq123d 4294 . . . . . . 7  |-  ( ph  ->  ( ( F `  z ) G w  <-> 
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w ) )
3631, 35anbi12d 703 . . . . . 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 2569 . . . . . . . . 9  |-  F/_ x
z
38 nfv 1672 . . . . . . . . . 10  |-  F/ x ph
39 nffvmpt1 5687 . . . . . . . . . . . 12  |-  F/_ x
( ( x  e.  A  |->  R ) `  z )
40 nfcv 2569 . . . . . . . . . . . 12  |-  F/_ x
( y  e.  B  |->  S )
41 nfcv 2569 . . . . . . . . . . . 12  |-  F/_ x w
4239, 40, 41nfbr 4324 . . . . . . . . . . 11  |-  F/ x
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w
43 nfcsb1v 3292 . . . . . . . . . . . 12  |-  F/_ x [_ z  /  x ]_ T
4443nfeq2 2580 . . . . . . . . . . 11  |-  F/ x  w  =  [_ z  /  x ]_ T
4542, 44nfbi 1865 . . . . . . . . . 10  |-  F/ x
( ( ( x  e.  A  |->  R ) `
 z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T )
4638, 45nfim 1851 . . . . . . . . 9  |-  F/ x
( ph  ->  ( ( ( x  e.  A  |->  R ) `  z
) ( y  e.  B  |->  S ) w  <-> 
w  =  [_ z  /  x ]_ T ) )
47 fveq2 5679 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( x  e.  A  |->  R ) `  x
)  =  ( ( x  e.  A  |->  R ) `  z ) )
4847breq1d 4290 . . . . . . . . . . 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 3285 . . . . . . . . . . . 12  |-  ( x  =  z  ->  T  =  [_ z  /  x ]_ T )
5049eqeq2d 2444 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
w  =  T  <->  w  =  [_ z  /  x ]_ T ) )
5148, 50bibi12d 321 . . . . . . . . . 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 316 . . . . . . . . 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 2965 . . . . . . . . . . . 12  |-  w  e. 
_V
54 simpl 454 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  y  =  R )
5554eleq1d 2499 . . . . . . . . . . . . . 14  |-  ( ( y  =  R  /\  u  =  w )  ->  ( y  e.  B  <->  R  e.  B ) )
56 simpr 458 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  u  =  w )
57 fmptco.4 . . . . . . . . . . . . . . . 16  |-  ( y  =  R  ->  S  =  T )
5857adantr 462 . . . . . . . . . . . . . . 15  |-  ( ( y  =  R  /\  u  =  w )  ->  S  =  T )
5956, 58eqeq12d 2447 . . . . . . . . . . . . . 14  |-  ( ( y  =  R  /\  u  =  w )  ->  ( u  =  S  <-> 
w  =  T ) )
6055, 59anbi12d 703 . . . . . . . . . . . . 13  |-  ( ( y  =  R  /\  u  =  w )  ->  ( ( y  e.  B  /\  u  =  S )  <->  ( R  e.  B  /\  w  =  T ) ) )
61 df-mpt 4340 . . . . . . . . . . . . 13  |-  ( y  e.  B  |->  S )  =  { <. y ,  u >.  |  (
y  e.  B  /\  u  =  S ) }
6260, 61brabga 4592 . . . . . . . . . . . 12  |-  ( ( R  e.  B  /\  w  e.  _V )  ->  ( R ( y  e.  B  |->  S ) w  <->  ( R  e.  B  /\  w  =  T ) ) )
635, 53, 62sylancl 655 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ( R ( y  e.  B  |->  S ) w  <-> 
( R  e.  B  /\  w  =  T
) ) )
64 simpr 458 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
656fvmpt2 5769 . . . . . . . . . . . . 13  |-  ( ( x  e.  A  /\  R  e.  B )  ->  ( ( x  e.  A  |->  R ) `  x )  =  R )
6664, 5, 65syl2anc 654 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  R ) `  x
)  =  R )
6766breq1d 4290 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  R ( y  e.  B  |->  S ) w ) )
685biantrurd 505 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
w  =  T  <->  ( R  e.  B  /\  w  =  T ) ) )
6963, 67, 683bitr4d 285 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  w  =  T
) )
7069expcom 435 . . . . . . . . 9  |-  ( x  e.  A  ->  ( ph  ->  ( ( ( x  e.  A  |->  R ) `  x ) ( y  e.  B  |->  S ) w  <->  w  =  T ) ) )
7137, 46, 52, 70vtoclgaf 3024 . . . . . . . 8  |-  ( z  e.  A  ->  ( ph  ->  ( ( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T ) ) )
7271impcom 430 . . . . . . 7  |-  ( (
ph  /\  z  e.  A )  ->  (
( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w  <->  w  =  [_ z  /  x ]_ T ) )
7372pm5.32da 634 . . . . . 6  |-  ( ph  ->  ( ( z  e.  A  /\  ( ( x  e.  A  |->  R ) `  z ) ( y  e.  B  |->  S ) w )  <-> 
( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
7436, 73bitrd 253 . . . . 5  |-  ( ph  ->  ( ( z F ( F `  z
)  /\  ( F `  z ) G w )  <->  ( z  e.  A  /\  w  = 
[_ z  /  x ]_ T ) ) )
7525, 74syl5bb 257 . . . 4  |-  ( ph  ->  ( E. u ( u  =  ( F `
 z )  /\  ( z F u  /\  u G w ) )  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
7620, 75bitrd 253 . . 3  |-  ( ph  ->  ( E. u ( z F u  /\  u G w )  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
77 vex 2965 . . . 4  |-  z  e. 
_V
7877, 53opelco 4998 . . 3  |-  ( <.
z ,  w >.  e.  ( G  o.  F
)  <->  E. u ( z F u  /\  u G w ) )
79 df-mpt 4340 . . . . 5  |-  ( x  e.  A  |->  T )  =  { <. x ,  v >.  |  ( x  e.  A  /\  v  =  T ) }
8079eleq2i 2497 . . . 4  |-  ( <.
z ,  w >.  e.  ( x  e.  A  |->  T )  <->  <. z ,  w >.  e.  { <. x ,  v >.  |  ( x  e.  A  /\  v  =  T ) } )
81 nfv 1672 . . . . . 6  |-  F/ x  z  e.  A
8243nfeq2 2580 . . . . . 6  |-  F/ x  v  =  [_ z  /  x ]_ T
8381, 82nfan 1859 . . . . 5  |-  F/ x
( z  e.  A  /\  v  =  [_ z  /  x ]_ T )
84 nfv 1672 . . . . 5  |-  F/ v ( z  e.  A  /\  w  =  [_ z  /  x ]_ T )
85 eleq1 2493 . . . . . 6  |-  ( x  =  z  ->  (
x  e.  A  <->  z  e.  A ) )
8649eqeq2d 2444 . . . . . 6  |-  ( x  =  z  ->  (
v  =  T  <->  v  =  [_ z  /  x ]_ T ) )
8785, 86anbi12d 703 . . . . 5  |-  ( x  =  z  ->  (
( x  e.  A  /\  v  =  T
)  <->  ( z  e.  A  /\  v  = 
[_ z  /  x ]_ T ) ) )
88 eqeq1 2439 . . . . . 6  |-  ( v  =  w  ->  (
v  =  [_ z  /  x ]_ T  <->  w  =  [_ z  /  x ]_ T ) )
8988anbi2d 696 . . . . 5  |-  ( v  =  w  ->  (
( z  e.  A  /\  v  =  [_ z  /  x ]_ T )  <-> 
( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) ) )
9083, 84, 77, 53, 87, 89opelopabf 4602 . . . 4  |-  ( <.
z ,  w >.  e. 
{ <. x ,  v
>.  |  ( x  e.  A  /\  v  =  T ) }  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) )
9180, 90bitri 249 . . 3  |-  ( <.
z ,  w >.  e.  ( x  e.  A  |->  T )  <->  ( z  e.  A  /\  w  =  [_ z  /  x ]_ T ) )
9276, 78, 913bitr4g 288 . 2  |-  ( ph  ->  ( <. z ,  w >.  e.  ( G  o.  F )  <->  <. z ,  w >.  e.  (
x  e.  A  |->  T ) ) )
931, 4, 92eqrelrdv 4923 1  |-  ( ph  ->  ( G  o.  F
)  =  ( x  e.  A  |->  T ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1362   E.wex 1589    e. wcel 1755   _Vcvv 2962   [_csb 3276   <.cop 3871   class class class wbr 4280   {copab 4337    e. cmpt 4338   dom cdm 4827    o. ccom 4831   Rel wrel 4832   Fun wfun 5400   -->wf 5402   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-fv 5414
This theorem is referenced by:  fmptcof  5864  fcompt  5866  fcoconst  5867  ofco  6329  ccatco  12447  lo1o12  12995  rlimcn1  13050  rlimcn1b  13051  rlimdiv  13107  ackbijnn  13274  setcepi  14939  prf1st  14997  prf2nd  14998  hofcllem  15051  prdsidlem  15436  pws0g  15440  pwsco1mhm  15480  pwsco2mhm  15481  pwsinvg  15647  pwssub  15648  galactghm  15888  efginvrel1  16205  frgpup3lem  16254  gsumzf1o  16371  gsumzf1oOLD  16374  gsumconst  16406  gsumzmhm  16407  gsumzmhmOLD  16408  gsummhm2  16411  gsummhm2OLD  16412  gsumsub  16423  gsumsubOLD  16424  gsum2dlem2  16436  gsum2dOLD  16438  dprdfsub  16485  dprdfsubOLD  16492  lmhmvsca  17048  psrass1lem  17381  psrlinv  17402  psrcom  17415  evlslem2  17525  coe1fval3  17563  psropprmul  17591  coe1z  17615  coe1mul2  17621  coe1tm  17624  ply1coe  17643  frgpcyg  17848  evpmodpmf1o  17868  mhmvlin  18139  ofco2  18174  mdetleib2  18241  mdetralt  18256  smadiadetlem3  18316  ptrescn  19054  lmcn2  19064  qtopeu  19131  flfcnp2  19422  tgpconcomp  19525  tsmsmhm  19562  tsmssub  19565  tsmsxplem1  19569  negfcncf  20337  pcopt  20436  pcopt2  20437  pi1xfrcnvlem  20470  ovolctb  20815  ovolfs2  20893  uniioombllem2  20905  uniioombllem3  20907  ismbf  20950  mbfconst  20955  ismbfcn2  20959  itg1climres  21034  iblabslem  21147  iblabs  21148  bddmulibl  21158  limccnp  21208  limccnp2  21209  limcco  21210  dvcof  21264  dvcjbr  21265  dvcj  21266  dvfre  21267  dvmptcj  21284  dvmptco  21288  dvcnvlem  21290  dvef  21294  dvlip  21307  dvlipcn  21308  itgsubstlem  21362  plypf1  21565  plyco  21594  dgrcolem1  21625  dgrcolem2  21626  dgrco  21627  plycjlem  21628  taylply2  21718  logcn  21977  leibpi  22222  efrlim  22248  jensenlem2  22266  amgmlem  22268  ftalem7  22301  lgseisenlem4  22576  dchrisum0  22654  cofmpt  25805  gsummptmhm  26102  ofcfval4  26401  eulerpartgbij  26603  dstfrvclim1  26708  lgamgulmlem2  26864  lgamcvg2  26889  cvmliftlem6  27027  cvmliftphtlem  27054  cvmlift3lem5  27060  circum  27166  mblfinlem2  28273  volsupnfl  28280  itgaddnc  28296  itgmulc2nc  28304  ftc1anclem1  28311  ftc1anclem2  28312  ftc1anclem3  28313  ftc1anclem4  28314  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  fnopabco  28460  upixp  28467  mendassa  29396
  Copyright terms: Public domain W3C validator