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

Theorem fovrnd 6759
Description: An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
Hypotheses
Ref Expression
fovrnd.1 (𝜑𝐹:(𝑅 × 𝑆)⟶𝐶)
fovrnd.2 (𝜑𝐴𝑅)
fovrnd.3 (𝜑𝐵𝑆)
Assertion
Ref Expression
fovrnd (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶)

Proof of Theorem fovrnd
StepHypRef Expression
1 fovrnd.1 . 2 (𝜑𝐹:(𝑅 × 𝑆)⟶𝐶)
2 fovrnd.2 . 2 (𝜑𝐴𝑅)
3 fovrnd.3 . 2 (𝜑𝐵𝑆)
4 fovrn 6757 . 2 ((𝐹:(𝑅 × 𝑆)⟶𝐶𝐴𝑅𝐵𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
51, 2, 3, 4syl3anc 1323 1 (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987   × cxp 5072  wf 5843  (class class class)co 6604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-fv 5855  df-ov 6607
This theorem is referenced by:  eroveu  7787  fseqenlem1  8791  rlimcn2  14255  homarel  16607  curf1cl  16789  curf2cl  16792  hofcllem  16819  yonedalem3b  16840  gasubg  17656  gacan  17659  gapm  17660  gastacos  17664  orbsta  17667  galactghm  17744  sylow1lem2  17935  sylow2alem2  17954  sylow3lem1  17963  efgcpbllemb  18089  frgpuplem  18106  frlmbas3  20034  mamucl  20126  mamuass  20127  mamudi  20128  mamudir  20129  mamuvs1  20130  mamuvs2  20131  mamulid  20166  mamurid  20167  mamutpos  20183  matgsumcl  20185  mavmulcl  20272  mavmulass  20274  mdetleib2  20313  mdetf  20320  mdetdiaglem  20323  mdetrlin  20327  mdetrsca  20328  mdetralt  20333  mdetunilem7  20343  maducoeval2  20365  madugsum  20368  madurid  20369  tsmsxplem2  21867  isxmet2d  22042  ismet2  22048  prdsxmetlem  22083  comet  22228  ipcn  22953  ovoliunlem2  23178  itg1addlem4  23372  itg1addlem5  23373  mbfi1fseqlem5  23392  limccnp2  23562  midcl  25569  pstmxmet  29719  cvmlift2lem9  30998  isbnd3  33212  prdsbnd  33221  iscringd  33426  rmxycomplete  36959  rmxyadd  36963
  Copyright terms: Public domain W3C validator