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

Theorem fvco2 5555
Description: Value of a function composition. Similar to second part of Theorem 3H of [Enderton] p. 47. (Contributed by NM, 9-Oct-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear, 16-Oct-2014.)
Assertion
Ref Expression
fvco2  |-  ( ( G  Fn  A  /\  X  e.  A )  ->  ( ( F  o.  G ) `  X
)  =  ( F `
 ( G `  X ) ) )
Dummy variable  x is distinct from all other variables.

Proof of Theorem fvco2
StepHypRef Expression
1 fnsnfv 5543 . . . . . . 7  |-  ( ( G  Fn  A  /\  X  e.  A )  ->  { ( G `  X ) }  =  ( G " { X } ) )
21imaeq2d 5011 . . . . . 6  |-  ( ( G  Fn  A  /\  X  e.  A )  ->  ( F " {
( G `  X
) } )  =  ( F " ( G " { X }
) ) )
3 imaco 5176 . . . . . 6  |-  ( ( F  o.  G )
" { X }
)  =  ( F
" ( G " { X } ) )
42, 3syl6reqr 2335 . . . . 5  |-  ( ( G  Fn  A  /\  X  e.  A )  ->  ( ( F  o.  G ) " { X } )  =  ( F " { ( G `  X ) } ) )
54eqeq1d 2292 . . . 4  |-  ( ( G  Fn  A  /\  X  e.  A )  ->  ( ( ( F  o.  G ) " { X } )  =  { x }  <->  ( F " { ( G `  X ) } )  =  { x }
) )
65abbidv 2398 . . 3  |-  ( ( G  Fn  A  /\  X  e.  A )  ->  { x  |  ( ( F  o.  G
) " { X } )  =  {
x } }  =  { x  |  ( F " { ( G `
 X ) } )  =  { x } } )
76unieqd 3839 . 2  |-  ( ( G  Fn  A  /\  X  e.  A )  ->  U. { x  |  ( ( F  o.  G ) " { X } )  =  {
x } }  =  U. { x  |  ( F " { ( G `  X ) } )  =  {
x } } )
8 df-fv 5229 . 2  |-  ( ( F  o.  G ) `
 X )  = 
U. { x  |  ( ( F  o.  G ) " { X } )  =  {
x } }
9 df-fv 5229 . 2  |-  ( F `
 ( G `  X ) )  = 
U. { x  |  ( F " {
( G `  X
) } )  =  { x } }
107, 8, 93eqtr4g 2341 1  |-  ( ( G  Fn  A  /\  X  e.  A )  ->  ( ( F  o.  G ) `  X
)  =  ( F `
 ( G `  X ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1624    e. wcel 1685   {cab 2270   {csn 3641   U.cuni 3828   "cima 4691    o. ccom 4692    Fn wfn 5216   ` cfv 5221
This theorem is referenced by:  fvco  5556  fvco3  5557  fvco4i  5558  ofco  6058  curry1  6171  curry2  6174  smobeth  8203  fpwwe  8263  addpqnq  8557  mulpqnq  8560  revco  11483  ccatco  11484  isoval  13661  prdsidlem  14398  gsumwmhm  14461  prdsinvlem  14597  rngidval  15337  prdsmgp  15387  lmhmco  15794  chrrhm  16479  1stccnp  17182  prdstopn  17316  xpstopnlem2  17496  uniioombllem6  18937  evlslem1  19393  evlsvar  19401  0vfval  21154  rabren3dioph  26297  dsmmbas2  26602  dsmm0cl  26605  frlmbas  26622  frlmup3  26651  frlmup4  26652  enfixsn  26656  f1lindf  26691  lindfmm  26696  f1omvdconj  26788  pmtrfinv  26801  symggen  26810  symgtrinv  26812  hausgraph  26930  stoweidlem59  27207  afvco2  27414
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-id 4308  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-fv 5229
  Copyright terms: Public domain W3C validator