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

Theorem fovrnd 6431
Description: An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
Hypotheses
Ref Expression
fovrnd.1  |-  ( ph  ->  F : ( R  X.  S ) --> C )
fovrnd.2  |-  ( ph  ->  A  e.  R )
fovrnd.3  |-  ( ph  ->  B  e.  S )
Assertion
Ref Expression
fovrnd  |-  ( ph  ->  ( A F B )  e.  C )

Proof of Theorem fovrnd
StepHypRef Expression
1 fovrnd.1 . 2  |-  ( ph  ->  F : ( R  X.  S ) --> C )
2 fovrnd.2 . 2  |-  ( ph  ->  A  e.  R )
3 fovrnd.3 . 2  |-  ( ph  ->  B  e.  S )
4 fovrn 6429 . 2  |-  ( ( F : ( R  X.  S ) --> C  /\  A  e.  R  /\  B  e.  S
)  ->  ( A F B )  e.  C
)
51, 2, 3, 4syl3anc 1228 1  |-  ( ph  ->  ( A F B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767    X. cxp 4997   -->wf 5584  (class class class)co 6284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-fv 5596  df-ov 6287
This theorem is referenced by:  eroveu  7406  fseqenlem1  8405  rlimcn2  13376  homarel  15221  curf1cl  15355  curf2cl  15358  hofcllem  15385  yonedalem3b  15406  gasubg  16145  gacan  16148  gapm  16149  gastacos  16153  orbsta  16156  galactghm  16233  sylow1lem2  16425  sylow2alem2  16444  sylow3lem1  16453  efgcpbllemb  16579  frgpuplem  16596  frlmbas3  18602  mamucl  18698  mamuass  18699  mamudi  18700  mamudir  18701  mamuvs1  18702  mamuvs2  18703  mamulid  18738  mamurid  18739  mamutpos  18755  matgsumcl  18757  mavmulcl  18844  mavmulass  18846  mdetleib2  18885  mdetf  18892  mdetdiaglem  18895  mdetrlin  18899  mdetrsca  18900  mdetralt  18905  mdetunilem7  18915  maducoeval2  18937  maduf  18938  madugsum  18940  madurid  18941  tsmsxplem2  20419  isxmet2d  20593  ismet2  20599  prdsxmetlem  20634  comet  20779  ipcn  21449  ovoliunlem2  21677  itg1addlem4  21869  itg1addlem5  21870  mbfi1fseqlem5  21889  limccnp2  22059  midcl  23848  pstmxmet  27540  cvmlift2lem9  28424  isbnd3  29911  prdsbnd  29920  iscringd  30027  rmxycomplete  30485  rmxyadd  30489
  Copyright terms: Public domain W3C validator