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

Theorem off 6554
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:   ,   , ,   ,S,   , ,   , ,   , ,   , ,

Proof of Theorem off
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 off.2 . . . . 5
2 off.6 . . . . . . 7
3 inss1 3717 . . . . . . 7
42, 3eqsstr3i 3534 . . . . . 6
54sseli 3499 . . . . 5
6 ffvelrn 6029 . . . . 5
71, 5, 6syl2an 477 . . . 4
8 off.3 . . . . 5
9 inss2 3718 . . . . . . 7
102, 9eqsstr3i 3534 . . . . . 6
1110sseli 3499 . . . . 5
12 ffvelrn 6029 . . . . 5
138, 11, 12syl2an 477 . . . 4
14 off.1 . . . . . 6
1514ralrimivva 2878 . . . . 5
1615adantr 465 . . . 4
17 oveq1 6303 . . . . . 6
1817eleq1d 2526 . . . . 5
19 oveq2 6304 . . . . . 6
2019eleq1d 2526 . . . . 5
2118, 20rspc2va 3220 . . . 4
227, 13, 16, 21syl21anc 1227 . . 3
23 eqid 2457 . . 3
2422, 23fmptd 6055 . 2
25 ffn 5736 . . . . 5
261, 25syl 16 . . . 4
27 ffn 5736 . . . . 5
288, 27syl 16 . . . 4
29 off.4 . . . 4
30 off.5 . . . 4
31 eqidd 2458 . . . 4
32 eqidd 2458 . . . 4
3326, 28, 29, 30, 2, 31, 32offval 6547 . . 3
3433feq1d 5722 . 2
3524, 34mpbird 232 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807  i^icin 3474  e.cmpt 4510  Fnwfn 5588  -->wf 5589  `cfv 5593  (class class class)co 6296  oFcof 6538
This theorem is referenced by:  o1of2  13435  ghmplusg  16852  gsumzaddlem  16934  gsumzadd  16935  gsumzaddlemOLD  16936  gsumzaddOLD  16937  lcomf  17548  psrbagaddcl  18020  psrbagaddclOLD  18021  psraddcl  18036  psrvscacl  18046  psrbagev1  18177  psrbagev1OLD  18178  evlslem3  18183  frlmup1  18832  mndvcl  18893  tsmsadd  20649  mbfmulc2lem  22054  mbfaddlem  22067  i1fadd  22102  i1fmul  22103  itg1addlem4  22106  i1fmulclem  22109  i1fmulc  22110  mbfi1flimlem  22129  itg2mulclem  22153  itg2mulc  22154  itg2monolem1  22157  itg2addlem  22165  dvaddbr  22341  dvmulbr  22342  dvaddf  22345  dvmulf  22346  dv11cn  22402  plyaddlem  22612  coeeulem  22621  coeaddlem  22646  plydivlem4  22692  jensenlem2  23317  jensen  23318  basellem7  23360  basellem9  23362  dchrmulcl  23524  ofrn  27479  sibfof  28282  signshf  28545  itg2addnc  30069  ftc1anclem3  30092  ftc1anclem6  30095  ftc1anclem8  30097  mzpclall  30659  mzpindd  30678  expgrowth  31240  binomcxplemnotnn0  31261  dvdivcncf  31724  ofaddmndmap  32933  lfladdcl  34796  lflvscl  34802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6540
  Copyright terms: Public domain W3C validator