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

Theorem ofrfval 6088
Description: Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
Hypotheses
Ref Expression
offval.1  |-  ( ph  ->  F  Fn  A )
offval.2  |-  ( ph  ->  G  Fn  B )
offval.3  |-  ( ph  ->  A  e.  V )
offval.4  |-  ( ph  ->  B  e.  W )
offval.5  |-  ( A  i^i  B )  =  S
offval.6  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  =  C )
offval.7  |-  ( (
ph  /\  x  e.  B )  ->  ( G `  x )  =  D )
Assertion
Ref Expression
ofrfval  |-  ( ph  ->  ( F  o R R G  <->  A. x  e.  S  C R D ) )
Distinct variable groups:    x, A    x, F    x, G    ph, x    x, S    x, R
Allowed substitution hints:    B( x)    C( x)    D( x)    V( x)    W( x)

Proof of Theorem ofrfval
Dummy variables  f 
g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 offval.1 . . . 4  |-  ( ph  ->  F  Fn  A )
2 offval.3 . . . 4  |-  ( ph  ->  A  e.  V )
3 fnex 5743 . . . 4  |-  ( ( F  Fn  A  /\  A  e.  V )  ->  F  e.  _V )
41, 2, 3syl2anc 642 . . 3  |-  ( ph  ->  F  e.  _V )
5 offval.2 . . . 4  |-  ( ph  ->  G  Fn  B )
6 offval.4 . . . 4  |-  ( ph  ->  B  e.  W )
7 fnex 5743 . . . 4  |-  ( ( G  Fn  B  /\  B  e.  W )  ->  G  e.  _V )
85, 6, 7syl2anc 642 . . 3  |-  ( ph  ->  G  e.  _V )
9 dmeq 4881 . . . . . 6  |-  ( f  =  F  ->  dom  f  =  dom  F )
10 dmeq 4881 . . . . . 6  |-  ( g  =  G  ->  dom  g  =  dom  G )
119, 10ineqan12d 3374 . . . . 5  |-  ( ( f  =  F  /\  g  =  G )  ->  ( dom  f  i^i 
dom  g )  =  ( dom  F  i^i  dom 
G ) )
12 fveq1 5526 . . . . . 6  |-  ( f  =  F  ->  (
f `  x )  =  ( F `  x ) )
13 fveq1 5526 . . . . . 6  |-  ( g  =  G  ->  (
g `  x )  =  ( G `  x ) )
1412, 13breqan12d 4040 . . . . 5  |-  ( ( f  =  F  /\  g  =  G )  ->  ( ( f `  x ) R ( g `  x )  <-> 
( F `  x
) R ( G `
 x ) ) )
1511, 14raleqbidv 2750 . . . 4  |-  ( ( f  =  F  /\  g  =  G )  ->  ( A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x )  <->  A. x  e.  ( dom  F  i^i  dom 
G ) ( F `
 x ) R ( G `  x
) ) )
16 df-ofr 6081 . . . 4  |-  o R R  =  { <. f ,  g >.  |  A. x  e.  ( dom  f  i^i  dom  g )
( f `  x
) R ( g `
 x ) }
1715, 16brabga 4281 . . 3  |-  ( ( F  e.  _V  /\  G  e.  _V )  ->  ( F  o R R G  <->  A. x  e.  ( dom  F  i^i  dom 
G ) ( F `
 x ) R ( G `  x
) ) )
184, 8, 17syl2anc 642 . 2  |-  ( ph  ->  ( F  o R R G  <->  A. x  e.  ( dom  F  i^i  dom 
G ) ( F `
 x ) R ( G `  x
) ) )
19 fndm 5345 . . . . . 6  |-  ( F  Fn  A  ->  dom  F  =  A )
201, 19syl 15 . . . . 5  |-  ( ph  ->  dom  F  =  A )
21 fndm 5345 . . . . . 6  |-  ( G  Fn  B  ->  dom  G  =  B )
225, 21syl 15 . . . . 5  |-  ( ph  ->  dom  G  =  B )
2320, 22ineq12d 3373 . . . 4  |-  ( ph  ->  ( dom  F  i^i  dom 
G )  =  ( A  i^i  B ) )
24 offval.5 . . . 4  |-  ( A  i^i  B )  =  S
2523, 24syl6eq 2333 . . 3  |-  ( ph  ->  ( dom  F  i^i  dom 
G )  =  S )
2625raleqdv 2744 . 2  |-  ( ph  ->  ( A. x  e.  ( dom  F  i^i  dom 
G ) ( F `
 x ) R ( G `  x
)  <->  A. x  e.  S  ( F `  x ) R ( G `  x ) ) )
27 inss1 3391 . . . . . . 7  |-  ( A  i^i  B )  C_  A
2824, 27eqsstr3i 3211 . . . . . 6  |-  S  C_  A
2928sseli 3178 . . . . 5  |-  ( x  e.  S  ->  x  e.  A )
30 offval.6 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  =  C )
3129, 30sylan2 460 . . . 4  |-  ( (
ph  /\  x  e.  S )  ->  ( F `  x )  =  C )
32 inss2 3392 . . . . . . 7  |-  ( A  i^i  B )  C_  B
3324, 32eqsstr3i 3211 . . . . . 6  |-  S  C_  B
3433sseli 3178 . . . . 5  |-  ( x  e.  S  ->  x  e.  B )
35 offval.7 . . . . 5  |-  ( (
ph  /\  x  e.  B )  ->  ( G `  x )  =  D )
3634, 35sylan2 460 . . . 4  |-  ( (
ph  /\  x  e.  S )  ->  ( G `  x )  =  D )
3731, 36breq12d 4038 . . 3  |-  ( (
ph  /\  x  e.  S )  ->  (
( F `  x
) R ( G `
 x )  <->  C R D ) )
3837ralbidva 2561 . 2  |-  ( ph  ->  ( A. x  e.  S  ( F `  x ) R ( G `  x )  <->  A. x  e.  S  C R D ) )
3918, 26, 383bitrd 270 1  |-  ( ph  ->  ( F  o R R G  <->  A. x  e.  S  C R D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1625    e. wcel 1686   A.wral 2545   _Vcvv 2790    i^i cin 3153   class class class wbr 4025   dom cdm 4691    Fn wfn 5252   ` cfv 5257    o Rcofr 6079
This theorem is referenced by:  ofrval  6090  ofrfval2  6098  caofref  6105  caofrss  6112  caoftrn  6114  ofsubge0  9747  pwsle  13393  pwsleval  13394  psrbaglesupp  16116  psrbagcon  16119  psrbaglefi  16120  psrlidm  16150  0plef  19029  0pledm  19030  itg1ge0  19043  mbfi1fseqlem5  19076  xrge0f  19088  itg2ge0  19092  itg2lea  19101  itg2splitlem  19105  itg2monolem1  19107  itg2mono  19110  itg2i1fseqle  19111  itg2i1fseq  19112  itg2addlem  19115  itg2cnlem1  19118  itg2addnclem  24933  itg2addnc  24935
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ofr 6081
  Copyright terms: Public domain W3C validator