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 6662 | . . . 4 ⊢ (𝐹:(𝑅 × 𝑆)⟶𝐶 ↔ (𝐹 Fn (𝑅 × 𝑆) ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶)) | |
3 | 2 | simprbi 479 | . . 3 ⊢ (𝐹:(𝑅 × 𝑆)⟶𝐶 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶) |
4 | 1, 3 | ax-mp 5 | . 2 ⊢ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶 |
5 | oveq1 6556 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥𝐹𝑦) = (𝐴𝐹𝑦)) | |
6 | 5 | eleq1d 2672 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥𝐹𝑦) ∈ 𝐶 ↔ (𝐴𝐹𝑦) ∈ 𝐶)) |
7 | oveq2 6557 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝐴𝐹𝑦) = (𝐴𝐹𝐵)) | |
8 | 7 | eleq1d 2672 | . . 3 ⊢ (𝑦 = 𝐵 → ((𝐴𝐹𝑦) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶)) |
9 | 6, 8 | rspc2v 3293 | . 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶 → (𝐴𝐹𝐵) ∈ 𝐶)) |
10 | 4, 9 | mpi 20 | 1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∀wral 2896 × cxp 5036 Fn wfn 5799 ⟶wf 5800 (class class class)co 6549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-fv 5812 df-ov 6552 |
This theorem is referenced by: addclnq 9646 mulclnq 9648 adderpq 9657 mulerpq 9658 distrnq 9662 axaddcl 9851 axmulcl 9853 xaddcl 11944 xmulcl 11975 elfzoelz 12339 addcnlem 22475 sgmcl 24672 hvaddcl 27253 hvmulcl 27254 hicl 27321 hhssabloilem 27502 rmxynorm 36501 rmxyneg 36503 rmxy1 36505 rmxy0 36506 rmxp1 36515 rmyp1 36516 rmxm1 36517 rmym1 36518 rmxluc 36519 rmyluc 36520 rmyluc2 36521 rmxdbl 36522 rmydbl 36523 rmxypos 36532 ltrmynn0 36533 ltrmxnn0 36534 lermxnn0 36535 rmxnn 36536 ltrmy 36537 rmyeq0 36538 rmyeq 36539 lermy 36540 rmynn 36541 rmynn0 36542 rmyabs 36543 jm2.24nn 36544 jm2.17a 36545 jm2.17b 36546 jm2.17c 36547 jm2.24 36548 rmygeid 36549 jm2.18 36573 jm2.19lem1 36574 jm2.19lem2 36575 jm2.19 36578 jm2.22 36580 jm2.23 36581 jm2.20nn 36582 jm2.25 36584 jm2.26a 36585 jm2.26lem3 36586 jm2.26 36587 jm2.15nn0 36588 jm2.16nn0 36589 jm2.27a 36590 jm2.27c 36592 rmydioph 36599 rmxdiophlem 36600 jm3.1lem1 36602 jm3.1 36605 expdiophlem1 36606 |
Copyright terms: Public domain | W3C validator |