Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fovrnd | Structured version Visualization version GIF version |
Description: An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
Ref | Expression |
---|---|
fovrnd.1 | ⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶) |
fovrnd.2 | ⊢ (𝜑 → 𝐴 ∈ 𝑅) |
fovrnd.3 | ⊢ (𝜑 → 𝐵 ∈ 𝑆) |
Ref | Expression |
---|---|
fovrnd | ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fovrnd.1 | . 2 ⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶) | |
2 | fovrnd.2 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑅) | |
3 | fovrnd.3 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝑆) | |
4 | fovrn 7318 | . 2 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) | |
5 | 1, 2, 3, 4 | syl3anc 1367 | 1 ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 × cxp 5553 ⟶wf 6351 (class class class)co 7156 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pr 5330 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-fv 6363 df-ov 7159 |
This theorem is referenced by: eroveu 8392 fseqenlem1 9450 rlimcn2 14947 homarel 17296 curf1cl 17478 curf2cl 17481 hofcllem 17508 yonedalem3b 17529 gasubg 18432 gacan 18435 gapm 18436 gastacos 18440 orbsta 18443 galactghm 18532 sylow1lem2 18724 sylow2alem2 18743 sylow3lem1 18752 efgcpbllemb 18881 frgpuplem 18898 frlmbas3 20920 mamucl 21010 mamuass 21011 mamudi 21012 mamudir 21013 mamuvs1 21014 mamuvs2 21015 mamulid 21050 mamurid 21051 mamutpos 21067 matgsumcl 21069 mavmulcl 21156 mavmulass 21158 mdetleib2 21197 mdetf 21204 mdetdiaglem 21207 mdetrlin 21211 mdetrsca 21212 mdetralt 21217 mdetunilem7 21227 maducoeval2 21249 madugsum 21252 madurid 21253 tsmsxplem2 22762 isxmet2d 22937 ismet2 22943 prdsxmetlem 22978 comet 23123 ipcn 23849 ovoliunlem2 24104 itg1addlem4 24300 itg1addlem5 24301 mbfi1fseqlem5 24320 limccnp2 24490 midcl 26563 fedgmullem2 31026 pstmxmet 31137 cvmlift2lem9 32558 isbnd3 35077 prdsbnd 35086 iscringd 35291 rmxycomplete 39534 rmxyadd 39538 |
Copyright terms: Public domain | W3C validator |