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

Theorem off 7063
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 (𝜑 → (𝐹𝑓 𝑅𝐺):𝐶𝑈)
Distinct variable groups:   𝑦,𝐺   𝑥,𝑦,𝜑   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦   𝑥,𝐹,𝑦   𝑥,𝑅,𝑦   𝑥,𝑈,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐺(𝑥)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem off
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 off.2 . . . . 5 (𝜑𝐹:𝐴𝑆)
2 off.6 . . . . . . 7 (𝐴𝐵) = 𝐶
3 inss1 3981 . . . . . . 7 (𝐴𝐵) ⊆ 𝐴
42, 3eqsstr3i 3785 . . . . . 6 𝐶𝐴
54sseli 3748 . . . . 5 (𝑧𝐶𝑧𝐴)
6 ffvelrn 6502 . . . . 5 ((𝐹:𝐴𝑆𝑧𝐴) → (𝐹𝑧) ∈ 𝑆)
71, 5, 6syl2an 583 . . . 4 ((𝜑𝑧𝐶) → (𝐹𝑧) ∈ 𝑆)
8 off.3 . . . . 5 (𝜑𝐺:𝐵𝑇)
9 inss2 3982 . . . . . . 7 (𝐴𝐵) ⊆ 𝐵
102, 9eqsstr3i 3785 . . . . . 6 𝐶𝐵
1110sseli 3748 . . . . 5 (𝑧𝐶𝑧𝐵)
12 ffvelrn 6502 . . . . 5 ((𝐺:𝐵𝑇𝑧𝐵) → (𝐺𝑧) ∈ 𝑇)
138, 11, 12syl2an 583 . . . 4 ((𝜑𝑧𝐶) → (𝐺𝑧) ∈ 𝑇)
14 off.1 . . . . . 6 ((𝜑 ∧ (𝑥𝑆𝑦𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
1514ralrimivva 3120 . . . . 5 (𝜑 → ∀𝑥𝑆𝑦𝑇 (𝑥𝑅𝑦) ∈ 𝑈)
1615adantr 466 . . . 4 ((𝜑𝑧𝐶) → ∀𝑥𝑆𝑦𝑇 (𝑥𝑅𝑦) ∈ 𝑈)
17 oveq1 6803 . . . . . 6 (𝑥 = (𝐹𝑧) → (𝑥𝑅𝑦) = ((𝐹𝑧)𝑅𝑦))
1817eleq1d 2835 . . . . 5 (𝑥 = (𝐹𝑧) → ((𝑥𝑅𝑦) ∈ 𝑈 ↔ ((𝐹𝑧)𝑅𝑦) ∈ 𝑈))
19 oveq2 6804 . . . . . 6 (𝑦 = (𝐺𝑧) → ((𝐹𝑧)𝑅𝑦) = ((𝐹𝑧)𝑅(𝐺𝑧)))
2019eleq1d 2835 . . . . 5 (𝑦 = (𝐺𝑧) → (((𝐹𝑧)𝑅𝑦) ∈ 𝑈 ↔ ((𝐹𝑧)𝑅(𝐺𝑧)) ∈ 𝑈))
2118, 20rspc2va 3473 . . . 4 ((((𝐹𝑧) ∈ 𝑆 ∧ (𝐺𝑧) ∈ 𝑇) ∧ ∀𝑥𝑆𝑦𝑇 (𝑥𝑅𝑦) ∈ 𝑈) → ((𝐹𝑧)𝑅(𝐺𝑧)) ∈ 𝑈)
227, 13, 16, 21syl21anc 1475 . . 3 ((𝜑𝑧𝐶) → ((𝐹𝑧)𝑅(𝐺𝑧)) ∈ 𝑈)
2322fmpttd 6530 . 2 (𝜑 → (𝑧𝐶 ↦ ((𝐹𝑧)𝑅(𝐺𝑧))):𝐶𝑈)
241ffnd 6185 . . . 4 (𝜑𝐹 Fn 𝐴)
258ffnd 6185 . . . 4 (𝜑𝐺 Fn 𝐵)
26 off.4 . . . 4 (𝜑𝐴𝑉)
27 off.5 . . . 4 (𝜑𝐵𝑊)
28 eqidd 2772 . . . 4 ((𝜑𝑧𝐴) → (𝐹𝑧) = (𝐹𝑧))
29 eqidd 2772 . . . 4 ((𝜑𝑧𝐵) → (𝐺𝑧) = (𝐺𝑧))
3024, 25, 26, 27, 2, 28, 29offval 7055 . . 3 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑧𝐶 ↦ ((𝐹𝑧)𝑅(𝐺𝑧))))
3130feq1d 6169 . 2 (𝜑 → ((𝐹𝑓 𝑅𝐺):𝐶𝑈 ↔ (𝑧𝐶 ↦ ((𝐹𝑧)𝑅(𝐺𝑧))):𝐶𝑈))
3223, 31mpbird 247 1 (𝜑 → (𝐹𝑓 𝑅𝐺):𝐶𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  wcel 2145  wral 3061  cin 3722  cmpt 4864  wf 6026  cfv 6030  (class class class)co 6796  𝑓 cof 7046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pr 5035
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-ov 6799  df-oprab 6800  df-mpt2 6801  df-of 7048
This theorem is referenced by:  o1of2  14551  ghmplusg  18456  gsumzaddlem  18528  gsumzadd  18529  lcomf  19112  psrbagaddcl  19585  psraddcl  19598  psrvscacl  19608  psrbagev1  19725  evlslem3  19729  frlmup1  20354  mndvcl  20414  tsmsadd  22170  mbfmulc2lem  23634  mbfaddlem  23647  i1fadd  23682  i1fmul  23683  itg1addlem4  23686  i1fmulclem  23689  i1fmulc  23690  mbfi1flimlem  23709  itg2mulclem  23733  itg2mulc  23734  itg2monolem1  23737  itg2addlem  23745  dvaddbr  23921  dvmulbr  23922  dvaddf  23925  dvmulf  23926  dv11cn  23984  plyaddlem  24191  coeeulem  24200  coeaddlem  24225  plydivlem4  24271  jensenlem2  24935  jensen  24936  basellem7  25034  basellem9  25036  dchrmulcl  25195  ofrn  29781  sibfof  30742  signshf  31005  circlemethhgt  31061  poimirlem23  33764  poimirlem24  33765  poimirlem25  33766  poimirlem29  33770  poimirlem30  33771  poimirlem31  33772  poimirlem32  33773  itg2addnc  33795  ftc1anclem3  33818  ftc1anclem6  33821  ftc1anclem8  33823  lfladdcl  34878  lflvscl  34884  mzpclall  37814  mzpindd  37833  expgrowth  39058  binomcxplemnotnn0  39079  dvdivcncf  40655  ofaddmndmap  42645  amgmwlem  43074
  Copyright terms: Public domain W3C validator