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

Theorem fovcdm 7579
Description: An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)
Assertion
Ref Expression
fovcdm ((𝐹:(𝑅 × 𝑆)⟶𝐶𝐴𝑅𝐵𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)

Proof of Theorem fovcdm
StepHypRef Expression
1 opelxpi 5712 . . 3 ((𝐴𝑅𝐵𝑆) → ⟨𝐴, 𝐵⟩ ∈ (𝑅 × 𝑆))
2 df-ov 7414 . . . 4 (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3 ffvelcdm 7082 . . . 4 ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ ⟨𝐴, 𝐵⟩ ∈ (𝑅 × 𝑆)) → (𝐹‘⟨𝐴, 𝐵⟩) ∈ 𝐶)
42, 3eqeltrid 2835 . . 3 ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ ⟨𝐴, 𝐵⟩ ∈ (𝑅 × 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶)
51, 4sylan2 591 . 2 ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ (𝐴𝑅𝐵𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶)
653impb 1113 1 ((𝐹:(𝑅 × 𝑆)⟶𝐶𝐴𝑅𝐵𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1085  wcel 2104  cop 4633   × cxp 5673  wf 6538  cfv 6542  (class class class)co 7411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7414
This theorem is referenced by:  fovcdmda  7580  fovcdmd  7581  ovmpoelrn  8060  curry1f  8094  curry2f  8096  mapxpen  9145  axdc4lem  10452  axdc4uzlem  13952  imasmnd2  18696  grpsubcl  18939  imasgrp2  18974  imasring  20218  tsmsxplem1  23877  psmetcl  24033  xmetcl  24057  metcl  24058  blssm  24144  mbfi1fseqlem3  25467  mbfi1fseqlem4  25468  mbfi1fseqlem5  25469  grpocl  30020  grpodivcl  30059  vccl  30083  nvmcl  30166  cvmliftphtlem  34606  matunitlindflem1  36787  isbnd3  36955  clmgmOLD  37022  rngocl  37072  isdrngo2  37129
  Copyright terms: Public domain W3C validator