| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fovcdm | Structured version Visualization version GIF version | ||
| Description: An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.) |
| Ref | Expression |
|---|---|
| fovcdm | ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opelxpi 5659 | . . 3 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → 〈𝐴, 𝐵〉 ∈ (𝑅 × 𝑆)) | |
| 2 | df-ov 7361 | . . . 4 ⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | |
| 3 | ffvelcdm 7025 | . . . 4 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 〈𝐴, 𝐵〉 ∈ (𝑅 × 𝑆)) → (𝐹‘〈𝐴, 𝐵〉) ∈ 𝐶) | |
| 4 | 2, 3 | eqeltrid 2841 | . . 3 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 〈𝐴, 𝐵〉 ∈ (𝑅 × 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶) |
| 5 | 1, 4 | sylan2 594 | . 2 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶) |
| 6 | 5 | 3impb 1115 | 1 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 ∈ wcel 2114 〈cop 4574 × cxp 5620 ⟶wf 6486 ‘cfv 6490 (class class class)co 7358 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-nul 5241 ax-pr 5368 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-opab 5149 df-id 5517 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-fv 6498 df-ov 7361 |
| This theorem is referenced by: fovcdmda 7529 fovcdmd 7530 ovmpoelrn 8016 curry1f 8047 curry2f 8049 mapxpen 9072 axdc4lem 10366 axdc4uzlem 13907 imasmnd2 18700 grpsubcl 18954 imasgrp2 18989 imasring 20268 tsmsxplem1 24096 psmetcl 24250 xmetcl 24274 metcl 24275 blssm 24361 mbfi1fseqlem3 25662 mbfi1fseqlem4 25663 mbfi1fseqlem5 25664 grpocl 30560 grpodivcl 30599 vccl 30623 nvmcl 30706 cvmliftphtlem 35505 matunitlindflem1 37928 isbnd3 38096 clmgmOLD 38163 rngocl 38213 isdrngo2 38270 |
| Copyright terms: Public domain | W3C validator |