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 7281 | . . . 4 ⊢ (𝐹:(𝑅 × 𝑆)⟶𝐶 ↔ (𝐹 Fn (𝑅 × 𝑆) ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶)) | |
3 | 2 | simprbi 499 | . . 3 ⊢ (𝐹:(𝑅 × 𝑆)⟶𝐶 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶) |
4 | 1, 3 | ax-mp 5 | . 2 ⊢ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶 |
5 | oveq1 7166 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥𝐹𝑦) = (𝐴𝐹𝑦)) | |
6 | 5 | eleq1d 2900 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥𝐹𝑦) ∈ 𝐶 ↔ (𝐴𝐹𝑦) ∈ 𝐶)) |
7 | oveq2 7167 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝐴𝐹𝑦) = (𝐴𝐹𝐵)) | |
8 | 7 | eleq1d 2900 | . . 3 ⊢ (𝑦 = 𝐵 → ((𝐴𝐹𝑦) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶)) |
9 | 6, 8 | rspc2v 3636 | . 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶 → (𝐴𝐹𝐵) ∈ 𝐶)) |
10 | 4, 9 | mpi 20 | 1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1536 ∈ wcel 2113 ∀wral 3141 × cxp 5556 Fn wfn 6353 ⟶wf 6354 (class class class)co 7159 |
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 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pr 5333 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ral 3146 df-rex 3147 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4842 df-iun 4924 df-br 5070 df-opab 5132 df-mpt 5150 df-id 5463 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-fv 6366 df-ov 7162 |
This theorem is referenced by: addclnq 10370 mulclnq 10372 adderpq 10381 mulerpq 10382 distrnq 10386 axaddcl 10576 axmulcl 10578 xaddcl 12635 xmulcl 12669 elfzoelz 13041 addcnlem 23475 sgmcl 25726 hvaddcl 28792 hvmulcl 28793 hicl 28860 hhssabloilem 29041 rmxynorm 39521 rmxyneg 39523 rmxy1 39525 rmxy0 39526 rmxp1 39535 rmyp1 39536 rmxm1 39537 rmym1 39538 rmxluc 39539 rmyluc 39540 rmyluc2 39541 rmxdbl 39542 rmydbl 39543 rmxypos 39550 ltrmynn0 39551 ltrmxnn0 39552 lermxnn0 39553 rmxnn 39554 ltrmy 39555 rmyeq0 39556 rmyeq 39557 lermy 39558 rmynn 39559 rmynn0 39560 rmyabs 39561 jm2.24nn 39562 jm2.17a 39563 jm2.17b 39564 jm2.17c 39565 jm2.24 39566 rmygeid 39567 jm2.18 39591 jm2.19lem1 39592 jm2.19lem2 39593 jm2.19 39596 jm2.22 39598 jm2.23 39599 jm2.20nn 39600 jm2.25 39602 jm2.26a 39603 jm2.26lem3 39604 jm2.26 39605 jm2.15nn0 39606 jm2.16nn0 39607 jm2.27a 39608 jm2.27c 39610 rmydioph 39617 rmxdiophlem 39618 jm3.1lem1 39620 jm3.1 39623 expdiophlem1 39624 |
Copyright terms: Public domain | W3C validator |