MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fovcl Structured version   Visualization version   GIF version

Theorem fovcl 7273
Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
Hypothesis
Ref Expression
fovcl.1 𝐹:(𝑅 × 𝑆)⟶𝐶
Assertion
Ref Expression
fovcl ((𝐴𝑅𝐵𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)

Proof of Theorem fovcl
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fovcl.1 . . 3 𝐹:(𝑅 × 𝑆)⟶𝐶
2 ffnov 7272 . . . 4 (𝐹:(𝑅 × 𝑆)⟶𝐶 ↔ (𝐹 Fn (𝑅 × 𝑆) ∧ ∀𝑥𝑅𝑦𝑆 (𝑥𝐹𝑦) ∈ 𝐶))
32simprbi 497 . . 3 (𝐹:(𝑅 × 𝑆)⟶𝐶 → ∀𝑥𝑅𝑦𝑆 (𝑥𝐹𝑦) ∈ 𝐶)
41, 3ax-mp 5 . 2 𝑥𝑅𝑦𝑆 (𝑥𝐹𝑦) ∈ 𝐶
5 oveq1 7157 . . . 4 (𝑥 = 𝐴 → (𝑥𝐹𝑦) = (𝐴𝐹𝑦))
65eleq1d 2902 . . 3 (𝑥 = 𝐴 → ((𝑥𝐹𝑦) ∈ 𝐶 ↔ (𝐴𝐹𝑦) ∈ 𝐶))
7 oveq2 7158 . . . 4 (𝑦 = 𝐵 → (𝐴𝐹𝑦) = (𝐴𝐹𝐵))
87eleq1d 2902 . . 3 (𝑦 = 𝐵 → ((𝐴𝐹𝑦) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶))
96, 8rspc2v 3637 . 2 ((𝐴𝑅𝐵𝑆) → (∀𝑥𝑅𝑦𝑆 (𝑥𝐹𝑦) ∈ 𝐶 → (𝐴𝐹𝐵) ∈ 𝐶))
104, 9mpi 20 1 ((𝐴𝑅𝐵𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2107  wral 3143   × cxp 5552   Fn wfn 6349  wf 6350  (class class class)co 7150
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-fv 6362  df-ov 7153
This theorem is referenced by:  addclnq  10361  mulclnq  10363  adderpq  10372  mulerpq  10373  distrnq  10377  axaddcl  10567  axmulcl  10569  xaddcl  12627  xmulcl  12661  elfzoelz  13033  addcnlem  23406  sgmcl  25656  hvaddcl  28722  hvmulcl  28723  hicl  28790  hhssabloilem  28971  rmxynorm  39399  rmxyneg  39401  rmxy1  39403  rmxy0  39404  rmxp1  39413  rmyp1  39414  rmxm1  39415  rmym1  39416  rmxluc  39417  rmyluc  39418  rmyluc2  39419  rmxdbl  39420  rmydbl  39421  rmxypos  39428  ltrmynn0  39429  ltrmxnn0  39430  lermxnn0  39431  rmxnn  39432  ltrmy  39433  rmyeq0  39434  rmyeq  39435  lermy  39436  rmynn  39437  rmynn0  39438  rmyabs  39439  jm2.24nn  39440  jm2.17a  39441  jm2.17b  39442  jm2.17c  39443  jm2.24  39444  rmygeid  39445  jm2.18  39469  jm2.19lem1  39470  jm2.19lem2  39471  jm2.19  39474  jm2.22  39476  jm2.23  39477  jm2.20nn  39478  jm2.25  39480  jm2.26a  39481  jm2.26lem3  39482  jm2.26  39483  jm2.15nn0  39484  jm2.16nn0  39485  jm2.27a  39486  jm2.27c  39488  rmydioph  39495  rmxdiophlem  39496  jm3.1lem1  39498  jm3.1  39501  expdiophlem1  39502
  Copyright terms: Public domain W3C validator