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

Theorem off 6355
Description: The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
off.1  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  T ) )  -> 
( x R y )  e.  U )
off.2  |-  ( ph  ->  F : A --> S )
off.3  |-  ( ph  ->  G : B --> T )
off.4  |-  ( ph  ->  A  e.  V )
off.5  |-  ( ph  ->  B  e.  W )
off.6  |-  ( A  i^i  B )  =  C
Assertion
Ref Expression
off  |-  ( ph  ->  ( F  oF R G ) : C --> U )
Distinct variable groups:    y, G    x, y, ph    x, S, y   
x, T, y    x, F, y    x, R, y   
x, U, y
Allowed substitution hints:    A( x, y)    B( x, y)    C( x, y)    G( x)    V( x, y)    W( x, y)

Proof of Theorem off
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 off.2 . . . . 5  |-  ( ph  ->  F : A --> S )
2 off.6 . . . . . . 7  |-  ( A  i^i  B )  =  C
3 inss1 3591 . . . . . . 7  |-  ( A  i^i  B )  C_  A
42, 3eqsstr3i 3408 . . . . . 6  |-  C  C_  A
54sseli 3373 . . . . 5  |-  ( z  e.  C  ->  z  e.  A )
6 ffvelrn 5862 . . . . 5  |-  ( ( F : A --> S  /\  z  e.  A )  ->  ( F `  z
)  e.  S )
71, 5, 6syl2an 477 . . . 4  |-  ( (
ph  /\  z  e.  C )  ->  ( F `  z )  e.  S )
8 off.3 . . . . 5  |-  ( ph  ->  G : B --> T )
9 inss2 3592 . . . . . . 7  |-  ( A  i^i  B )  C_  B
102, 9eqsstr3i 3408 . . . . . 6  |-  C  C_  B
1110sseli 3373 . . . . 5  |-  ( z  e.  C  ->  z  e.  B )
12 ffvelrn 5862 . . . . 5  |-  ( ( G : B --> T  /\  z  e.  B )  ->  ( G `  z
)  e.  T )
138, 11, 12syl2an 477 . . . 4  |-  ( (
ph  /\  z  e.  C )  ->  ( G `  z )  e.  T )
14 off.1 . . . . . 6  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  T ) )  -> 
( x R y )  e.  U )
1514ralrimivva 2829 . . . . 5  |-  ( ph  ->  A. x  e.  S  A. y  e.  T  ( x R y )  e.  U )
1615adantr 465 . . . 4  |-  ( (
ph  /\  z  e.  C )  ->  A. x  e.  S  A. y  e.  T  ( x R y )  e.  U )
17 oveq1 6119 . . . . . 6  |-  ( x  =  ( F `  z )  ->  (
x R y )  =  ( ( F `
 z ) R y ) )
1817eleq1d 2509 . . . . 5  |-  ( x  =  ( F `  z )  ->  (
( x R y )  e.  U  <->  ( ( F `  z ) R y )  e.  U ) )
19 oveq2 6120 . . . . . 6  |-  ( y  =  ( G `  z )  ->  (
( F `  z
) R y )  =  ( ( F `
 z ) R ( G `  z
) ) )
2019eleq1d 2509 . . . . 5  |-  ( y  =  ( G `  z )  ->  (
( ( F `  z ) R y )  e.  U  <->  ( ( F `  z ) R ( G `  z ) )  e.  U ) )
2118, 20rspc2va 3101 . . . 4  |-  ( ( ( ( F `  z )  e.  S  /\  ( G `  z
)  e.  T )  /\  A. x  e.  S  A. y  e.  T  ( x R y )  e.  U
)  ->  ( ( F `  z ) R ( G `  z ) )  e.  U )
227, 13, 16, 21syl21anc 1217 . . 3  |-  ( (
ph  /\  z  e.  C )  ->  (
( F `  z
) R ( G `
 z ) )  e.  U )
23 eqid 2443 . . 3  |-  ( z  e.  C  |->  ( ( F `  z ) R ( G `  z ) ) )  =  ( z  e.  C  |->  ( ( F `
 z ) R ( G `  z
) ) )
2422, 23fmptd 5888 . 2  |-  ( ph  ->  ( z  e.  C  |->  ( ( F `  z ) R ( G `  z ) ) ) : C --> U )
25 ffn 5580 . . . . 5  |-  ( F : A --> S  ->  F  Fn  A )
261, 25syl 16 . . . 4  |-  ( ph  ->  F  Fn  A )
27 ffn 5580 . . . . 5  |-  ( G : B --> T  ->  G  Fn  B )
288, 27syl 16 . . . 4  |-  ( ph  ->  G  Fn  B )
29 off.4 . . . 4  |-  ( ph  ->  A  e.  V )
30 off.5 . . . 4  |-  ( ph  ->  B  e.  W )
31 eqidd 2444 . . . 4  |-  ( (
ph  /\  z  e.  A )  ->  ( F `  z )  =  ( F `  z ) )
32 eqidd 2444 . . . 4  |-  ( (
ph  /\  z  e.  B )  ->  ( G `  z )  =  ( G `  z ) )
3326, 28, 29, 30, 2, 31, 32offval 6348 . . 3  |-  ( ph  ->  ( F  oF R G )  =  ( z  e.  C  |->  ( ( F `  z ) R ( G `  z ) ) ) )
3433feq1d 5567 . 2  |-  ( ph  ->  ( ( F  oF R G ) : C --> U  <->  ( z  e.  C  |->  ( ( F `  z ) R ( G `  z ) ) ) : C --> U ) )
3524, 34mpbird 232 1  |-  ( ph  ->  ( F  oF R G ) : C --> U )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2736    i^i cin 3348    e. cmpt 4371    Fn wfn 5434   -->wf 5435   ` cfv 5439  (class class class)co 6112    oFcof 6339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pr 4552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-id 4657  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-of 6341
This theorem is referenced by:  o1of2  13111  ghmplusg  16349  gsumzaddlem  16429  gsumzadd  16430  gsumzaddlemOLD  16431  gsumzaddOLD  16432  lcomf  17005  psrbagaddcl  17460  psrbagaddclOLD  17461  psraddcl  17476  psrvscacl  17486  psrbagev1  17616  psrbagev1OLD  17617  evlslem3  17622  frlmup1  18248  mndvcl  18313  tsmsadd  19743  mbfmulc2lem  21147  mbfaddlem  21160  i1fadd  21195  i1fmul  21196  itg1addlem4  21199  i1fmulclem  21202  i1fmulc  21203  mbfi1flimlem  21222  itg2mulclem  21246  itg2mulc  21247  itg2monolem1  21250  itg2addlem  21258  dvaddbr  21434  dvmulbr  21435  dvaddf  21438  dvmulf  21439  dv11cn  21495  plyaddlem  21705  coeeulem  21714  coeaddlem  21738  plydivlem4  21784  jensenlem2  22403  jensen  22404  basellem7  22446  basellem9  22448  dchrmulcl  22610  ofrn  25979  sibfof  26748  signshf  27011  itg2addnc  28472  ftc1anclem3  28495  ftc1anclem6  28498  ftc1anclem8  28500  mzpclall  29089  mzpindd  29108  expgrowth  29635  ofaddmndmap  30761  lfladdcl  32812  lflvscl  32818
  Copyright terms: Public domain W3C validator