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

Theorem fovrnd 6446
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 6444 . 2  |-  ( ( F : ( R  X.  S ) --> C  /\  A  e.  R  /\  B  e.  S
)  ->  ( A F B )  e.  C
)
51, 2, 3, 4syl3anc 1264 1  |-  ( ph  ->  ( A F B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867    X. cxp 4843   -->wf 5588  (class class class)co 6296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-id 4760  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-fv 5600  df-ov 6299
This theorem is referenced by:  eroveu  7457  fseqenlem1  8444  rlimcn2  13621  homarel  15875  curf1cl  16057  curf2cl  16060  hofcllem  16087  yonedalem3b  16108  gasubg  16900  gacan  16903  gapm  16904  gastacos  16908  orbsta  16911  galactghm  16988  sylow1lem2  17179  sylow2alem2  17198  sylow3lem1  17207  efgcpbllemb  17333  frgpuplem  17350  frlmbas3  19258  mamucl  19350  mamuass  19351  mamudi  19352  mamudir  19353  mamuvs1  19354  mamuvs2  19355  mamulid  19390  mamurid  19391  mamutpos  19407  matgsumcl  19409  mavmulcl  19496  mavmulass  19498  mdetleib2  19537  mdetf  19544  mdetdiaglem  19547  mdetrlin  19551  mdetrsca  19552  mdetralt  19557  mdetunilem7  19567  maducoeval2  19589  madugsum  19592  madurid  19593  tsmsxplem2  21092  isxmet2d  21266  ismet2  21272  prdsxmetlem  21307  comet  21452  ipcn  22123  ovoliunlem2  22350  itg1addlem4  22551  itg1addlem5  22552  mbfi1fseqlem5  22571  limccnp2  22741  midcl  24701  pstmxmet  28565  cvmlift2lem9  29848  isbnd3  31849  prdsbnd  31858  iscringd  31965  rmxycomplete  35504  rmxyadd  35508
  Copyright terms: Public domain W3C validator