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

Theorem fovcl 6384
Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
Hypothesis
Ref Expression
fovcl.1  |-  F :
( R  X.  S
) --> C
Assertion
Ref Expression
fovcl  |-  ( ( A  e.  R  /\  B  e.  S )  ->  ( A F B )  e.  C )

Proof of Theorem fovcl
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fovcl.1 . . 3  |-  F :
( R  X.  S
) --> C
2 ffnov 6383 . . . 4  |-  ( F : ( R  X.  S ) --> C  <->  ( F  Fn  ( R  X.  S
)  /\  A. x  e.  R  A. y  e.  S  ( x F y )  e.  C ) )
32simprbi 464 . . 3  |-  ( F : ( R  X.  S ) --> C  ->  A. x  e.  R  A. y  e.  S  ( x F y )  e.  C )
41, 3ax-mp 5 . 2  |-  A. x  e.  R  A. y  e.  S  ( x F y )  e.  C
5 oveq1 6284 . . . 4  |-  ( x  =  A  ->  (
x F y )  =  ( A F y ) )
65eleq1d 2531 . . 3  |-  ( x  =  A  ->  (
( x F y )  e.  C  <->  ( A F y )  e.  C ) )
7 oveq2 6285 . . . 4  |-  ( y  =  B  ->  ( A F y )  =  ( A F B ) )
87eleq1d 2531 . . 3  |-  ( y  =  B  ->  (
( A F y )  e.  C  <->  ( A F B )  e.  C
) )
96, 8rspc2v 3218 . 2  |-  ( ( A  e.  R  /\  B  e.  S )  ->  ( A. x  e.  R  A. y  e.  S  ( x F y )  e.  C  ->  ( A F B )  e.  C ) )
104, 9mpi 17 1  |-  ( ( A  e.  R  /\  B  e.  S )  ->  ( A F B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    e. wcel 1762   A.wral 2809    X. cxp 4992    Fn wfn 5576   -->wf 5577  (class class class)co 6277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pr 4681
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-iun 4322  df-br 4443  df-opab 4501  df-mpt 4502  df-id 4790  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-rn 5005  df-iota 5544  df-fun 5583  df-fn 5584  df-f 5585  df-fv 5589  df-ov 6280
This theorem is referenced by:  addclnq  9314  mulclnq  9316  adderpq  9325  mulerpq  9326  distrnq  9330  axaddcl  9519  axmulcl  9521  xaddcl  11427  xmulcl  11456  elfzoelz  11788  addcnlem  21098  sgmcl  23143  issubgoi  24976  ablomul  25021  hvaddcl  25593  hvmulcl  25594  hicl  25661  rmxynorm  30447  rmxyneg  30449  rmxy1  30451  rmxy0  30452  rmxp1  30461  rmyp1  30462  rmxm1  30463  rmym1  30464  rmxluc  30465  rmyluc  30466  rmyluc2  30467  rmxdbl  30468  rmydbl  30469  rmxypos  30478  ltrmynn0  30479  ltrmxnn0  30480  lermxnn0  30481  rmxnn  30482  ltrmy  30483  rmyeq0  30484  rmyeq  30485  lermy  30486  rmynn  30487  rmynn0  30488  rmyabs  30489  jm2.24nn  30490  jm2.17a  30491  jm2.17b  30492  jm2.17c  30493  jm2.24  30494  rmygeid  30495  jm2.18  30525  jm2.19lem1  30526  jm2.19lem2  30527  jm2.19  30530  jm2.22  30532  jm2.23  30533  jm2.20nn  30534  jm2.25  30536  jm2.26a  30537  jm2.26lem3  30538  jm2.26  30539  jm2.15nn0  30540  jm2.16nn0  30541  jm2.27a  30542  jm2.27c  30544  rmydioph  30551  rmxdiophlem  30552  jm3.1lem1  30554  jm3.1  30557  expdiophlem1  30558
  Copyright terms: Public domain W3C validator