Theorem fovcl 7489

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.

Step	Hyp	Ref	Expression
1		fovcl.1	. . 3 ⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶
2		ffnov 7488	. . . 4 ⊢ (𝐹:(𝑅 × 𝑆)⟶𝐶 ↔ (𝐹 Fn (𝑅 × 𝑆) ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶))
3	2	simprbi 497	. . 3 ⊢ (𝐹:(𝑅 × 𝑆)⟶𝐶 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶)
4	1, 3	ax-mp 5	. 2 ⊢ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶
5		oveq1 7369	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥𝐹𝑦) = (𝐴𝐹𝑦))
6	5	eleq1d 2817	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥𝐹𝑦) ∈ 𝐶 ↔ (𝐴𝐹𝑦) ∈ 𝐶))
7		oveq2 7370	. . . 4 ⊢ (𝑦 = 𝐵 → (𝐴𝐹𝑦) = (𝐴𝐹𝐵))
8	7	eleq1d 2817	. . 3 ⊢ (𝑦 = 𝐵 → ((𝐴𝐹𝑦) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶))
9	6, 8	rspc2v 3591	. 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶 → (𝐴𝐹𝐵) ∈ 𝐶))
10	4, 9	mpi 20	1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3060   × cxp 5636   Fn wfn 6496  ⟶wf 6497  (class class class)co 7362

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-fv 6509  df-ov 7365

This theorem is referenced by:  addclnq  10890  mulclnq  10892  adderpq  10901  mulerpq  10902  distrnq  10906  axaddcl  11096  axmulcl  11098  xaddcl  13168  xmulcl  13202  elfzoelz  13582  addcnlem  24264  sgmcl  26532  hvaddcl  30017  hvmulcl  30018  hicl  30085  hhssabloilem  30266  rmxynorm  41300  rmxyneg  41302  rmxy1  41304  rmxy0  41305  rmxp1  41314  rmyp1  41315  rmxm1  41316  rmym1  41317  rmxluc  41318  rmyluc  41319  rmyluc2  41320  rmxdbl  41321  rmydbl  41322  rmxypos  41329  ltrmynn0  41330  ltrmxnn0  41331  lermxnn0  41332  rmxnn  41333  ltrmy  41334  rmyeq0  41335  rmyeq  41336  lermy  41337  rmynn  41338  rmynn0  41339  rmyabs  41340  jm2.24nn  41341  jm2.17a  41342  jm2.17b  41343  jm2.17c  41344  jm2.24  41345  rmygeid  41346  jm2.18  41370  jm2.19lem1  41371  jm2.19lem2  41372  jm2.19  41375  jm2.22  41377  jm2.23  41378  jm2.20nn  41379  jm2.25  41381  jm2.26a  41382  jm2.26lem3  41383  jm2.26  41384  jm2.15nn0  41385  jm2.16nn0  41386  jm2.27a  41387  jm2.27c  41389  rmydioph  41396  rmxdiophlem  41397  jm3.1lem1  41399  jm3.1  41402  expdiophlem1  41403