![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fovcl | Structured version Visualization version GIF version |
Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007.) |
Ref | Expression |
---|---|
fovcl.1 | ⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶 |
Ref | Expression |
---|---|
fovcl | ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fovcl.1 | . . 3 ⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶 | |
2 | ffnov 7257 | . . . 4 ⊢ (𝐹:(𝑅 × 𝑆)⟶𝐶 ↔ (𝐹 Fn (𝑅 × 𝑆) ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶)) | |
3 | 2 | simprbi 500 | . . 3 ⊢ (𝐹:(𝑅 × 𝑆)⟶𝐶 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶) |
4 | 1, 3 | ax-mp 5 | . 2 ⊢ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶 |
5 | oveq1 7142 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥𝐹𝑦) = (𝐴𝐹𝑦)) | |
6 | 5 | eleq1d 2874 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥𝐹𝑦) ∈ 𝐶 ↔ (𝐴𝐹𝑦) ∈ 𝐶)) |
7 | oveq2 7143 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝐴𝐹𝑦) = (𝐴𝐹𝐵)) | |
8 | 7 | eleq1d 2874 | . . 3 ⊢ (𝑦 = 𝐵 → ((𝐴𝐹𝑦) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶)) |
9 | 6, 8 | rspc2v 3581 | . 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶 → (𝐴𝐹𝐵) ∈ 𝐶)) |
10 | 4, 9 | mpi 20 | 1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∀wral 3106 × cxp 5517 Fn wfn 6319 ⟶wf 6320 (class class class)co 7135 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-fv 6332 df-ov 7138 |
This theorem is referenced by: addclnq 10356 mulclnq 10358 adderpq 10367 mulerpq 10368 distrnq 10372 axaddcl 10562 axmulcl 10564 xaddcl 12620 xmulcl 12654 elfzoelz 13033 addcnlem 23469 sgmcl 25731 hvaddcl 28795 hvmulcl 28796 hicl 28863 hhssabloilem 29044 rmxynorm 39859 rmxyneg 39861 rmxy1 39863 rmxy0 39864 rmxp1 39873 rmyp1 39874 rmxm1 39875 rmym1 39876 rmxluc 39877 rmyluc 39878 rmyluc2 39879 rmxdbl 39880 rmydbl 39881 rmxypos 39888 ltrmynn0 39889 ltrmxnn0 39890 lermxnn0 39891 rmxnn 39892 ltrmy 39893 rmyeq0 39894 rmyeq 39895 lermy 39896 rmynn 39897 rmynn0 39898 rmyabs 39899 jm2.24nn 39900 jm2.17a 39901 jm2.17b 39902 jm2.17c 39903 jm2.24 39904 rmygeid 39905 jm2.18 39929 jm2.19lem1 39930 jm2.19lem2 39931 jm2.19 39934 jm2.22 39936 jm2.23 39937 jm2.20nn 39938 jm2.25 39940 jm2.26a 39941 jm2.26lem3 39942 jm2.26 39943 jm2.15nn0 39944 jm2.16nn0 39945 jm2.27a 39946 jm2.27c 39948 rmydioph 39955 rmxdiophlem 39956 jm3.1lem1 39958 jm3.1 39961 expdiophlem1 39962 |
Copyright terms: Public domain | W3C validator |