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

Theorem off 7714
Description: The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
off.1 ((𝜑 ∧ (𝑥𝑆𝑦𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
off.2 (𝜑𝐹:𝐴𝑆)
off.3 (𝜑𝐺:𝐵𝑇)
off.4 (𝜑𝐴𝑉)
off.5 (𝜑𝐵𝑊)
off.6 (𝐴𝐵) = 𝐶
Assertion
Ref Expression
off (𝜑 → (𝐹f 𝑅𝐺):𝐶𝑈)
Distinct variable groups:   𝑦,𝐺   𝑥,𝑦,𝜑   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦   𝑥,𝐹,𝑦   𝑥,𝑅,𝑦   𝑥,𝑈,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐺(𝑥)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem off
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 off.2 . . . 4 (𝜑𝐹:𝐴𝑆)
21ffnd 6737 . . 3 (𝜑𝐹 Fn 𝐴)
3 off.3 . . . 4 (𝜑𝐺:𝐵𝑇)
43ffnd 6737 . . 3 (𝜑𝐺 Fn 𝐵)
5 off.4 . . 3 (𝜑𝐴𝑉)
6 off.5 . . 3 (𝜑𝐵𝑊)
7 off.6 . . 3 (𝐴𝐵) = 𝐶
8 eqidd 2735 . . 3 ((𝜑𝑧𝐴) → (𝐹𝑧) = (𝐹𝑧))
9 eqidd 2735 . . 3 ((𝜑𝑧𝐵) → (𝐺𝑧) = (𝐺𝑧))
102, 4, 5, 6, 7, 8, 9offval 7705 . 2 (𝜑 → (𝐹f 𝑅𝐺) = (𝑧𝐶 ↦ ((𝐹𝑧)𝑅(𝐺𝑧))))
11 inss1 4244 . . . . . 6 (𝐴𝐵) ⊆ 𝐴
127, 11eqsstrri 4030 . . . . 5 𝐶𝐴
1312sseli 3990 . . . 4 (𝑧𝐶𝑧𝐴)
14 ffvelcdm 7100 . . . 4 ((𝐹:𝐴𝑆𝑧𝐴) → (𝐹𝑧) ∈ 𝑆)
151, 13, 14syl2an 596 . . 3 ((𝜑𝑧𝐶) → (𝐹𝑧) ∈ 𝑆)
16 inss2 4245 . . . . . 6 (𝐴𝐵) ⊆ 𝐵
177, 16eqsstrri 4030 . . . . 5 𝐶𝐵
1817sseli 3990 . . . 4 (𝑧𝐶𝑧𝐵)
19 ffvelcdm 7100 . . . 4 ((𝐺:𝐵𝑇𝑧𝐵) → (𝐺𝑧) ∈ 𝑇)
203, 18, 19syl2an 596 . . 3 ((𝜑𝑧𝐶) → (𝐺𝑧) ∈ 𝑇)
21 off.1 . . . . 5 ((𝜑 ∧ (𝑥𝑆𝑦𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
2221ralrimivva 3199 . . . 4 (𝜑 → ∀𝑥𝑆𝑦𝑇 (𝑥𝑅𝑦) ∈ 𝑈)
2322adantr 480 . . 3 ((𝜑𝑧𝐶) → ∀𝑥𝑆𝑦𝑇 (𝑥𝑅𝑦) ∈ 𝑈)
24 ovrspc2v 7456 . . 3 ((((𝐹𝑧) ∈ 𝑆 ∧ (𝐺𝑧) ∈ 𝑇) ∧ ∀𝑥𝑆𝑦𝑇 (𝑥𝑅𝑦) ∈ 𝑈) → ((𝐹𝑧)𝑅(𝐺𝑧)) ∈ 𝑈)
2515, 20, 23, 24syl21anc 838 . 2 ((𝜑𝑧𝐶) → ((𝐹𝑧)𝑅(𝐺𝑧)) ∈ 𝑈)
2610, 25fmpt3d 7135 1 (𝜑 → (𝐹f 𝑅𝐺):𝐶𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wcel 2105  wral 3058  cin 3961  wf 6558  cfv 6562  (class class class)co 7430  f cof 7694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696
This theorem is referenced by:  suppofssd  8226  o1of2  15645  mndvcl  18822  ghmplusg  19878  gsumzaddlem  19953  gsumzadd  19954  lcomf  20915  frlmup1  21835  psrbagaddcl  21961  psraddcl  21975  psraddclOLD  21976  psrvscacl  21988  psrbagev1  22118  evlslem3  22121  tsmsadd  24170  mbfmulc2lem  25695  mbfaddlem  25708  i1fadd  25743  i1fmul  25744  itg1addlem4  25747  itg1addlem4OLD  25748  i1fmulclem  25751  i1fmulc  25752  mbfi1flimlem  25771  itg2mulclem  25795  itg2mulc  25796  itg2monolem1  25799  itg2addlem  25807  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvaddf  25993  dvmulf  25994  dv11cn  26054  plyaddlem  26268  coeeulem  26277  coeaddlem  26302  plydivlem4  26352  jensenlem2  27045  jensen  27046  basellem7  27144  basellem9  27146  dchrmulcl  27307  ofrn  32655  offinsupp1  32744  elrgspnlem1  33231  1arithidomlem2  33543  1arithidom  33544  ply1degltdimlem  33649  fedgmullem1  33656  sibfof  34321  signshf  34581  circlemethhgt  34636  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  itg2addnc  37660  ftc1anclem3  37681  ftc1anclem6  37684  ftc1anclem8  37686  lfladdcl  39052  lflvscl  39058  fsuppssind  42579  mhphf  42583  mzpclall  42714  mzpindd  42733  expgrowth  44330  binomcxplemnotnn0  44351  dvdivcncf  45882  ofaddmndmap  48187  amgmwlem  49032
  Copyright terms: Public domain W3C validator