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

Theorem ofrfval 6173
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 5827 . . . 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 5827 . . . 4  |-  ( ( G  Fn  B  /\  B  e.  W )  ->  G  e.  _V )
85, 6, 7syl2anc 642 . . 3  |-  ( ph  ->  G  e.  _V )
9 dmeq 4961 . . . . . 6  |-  ( f  =  F  ->  dom  f  =  dom  F )
10 dmeq 4961 . . . . . 6  |-  ( g  =  G  ->  dom  g  =  dom  G )
119, 10ineqan12d 3448 . . . . 5  |-  ( ( f  =  F  /\  g  =  G )  ->  ( dom  f  i^i 
dom  g )  =  ( dom  F  i^i  dom 
G ) )
12 fveq1 5607 . . . . . 6  |-  ( f  =  F  ->  (
f `  x )  =  ( F `  x ) )
13 fveq1 5607 . . . . . 6  |-  ( g  =  G  ->  (
g `  x )  =  ( G `  x ) )
1412, 13breqan12d 4119 . . . . 5  |-  ( ( f  =  F  /\  g  =  G )  ->  ( ( f `  x ) R ( g `  x )  <-> 
( F `  x
) R ( G `
 x ) ) )
1511, 14raleqbidv 2824 . . . 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 6166 . . . 4  |-  o R R  =  { <. f ,  g >.  |  A. x  e.  ( dom  f  i^i  dom  g )
( f `  x
) R ( g `
 x ) }
1715, 16brabga 4361 . . 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 5425 . . . . . 6  |-  ( F  Fn  A  ->  dom  F  =  A )
201, 19syl 15 . . . . 5  |-  ( ph  ->  dom  F  =  A )
21 fndm 5425 . . . . . 6  |-  ( G  Fn  B  ->  dom  G  =  B )
225, 21syl 15 . . . . 5  |-  ( ph  ->  dom  G  =  B )
2320, 22ineq12d 3447 . . . 4  |-  ( ph  ->  ( dom  F  i^i  dom 
G )  =  ( A  i^i  B ) )
24 offval.5 . . . 4  |-  ( A  i^i  B )  =  S
2523, 24syl6eq 2406 . . 3  |-  ( ph  ->  ( dom  F  i^i  dom 
G )  =  S )
2625raleqdv 2818 . 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 3465 . . . . . . 7  |-  ( A  i^i  B )  C_  A
2824, 27eqsstr3i 3285 . . . . . 6  |-  S  C_  A
2928sseli 3252 . . . . 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 3466 . . . . . . 7  |-  ( A  i^i  B )  C_  B
3324, 32eqsstr3i 3285 . . . . . 6  |-  S  C_  B
3433sseli 3252 . . . . 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 4117 . . 3  |-  ( (
ph  /\  x  e.  S )  ->  (
( F `  x
) R ( G `
 x )  <->  C R D ) )
3837ralbidva 2635 . 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 1642    e. wcel 1710   A.wral 2619   _Vcvv 2864    i^i cin 3227   class class class wbr 4104   dom cdm 4771    Fn wfn 5332   ` cfv 5337    o Rcofr 6164
This theorem is referenced by:  ofrval  6175  ofrfval2  6183  caofref  6190  caofrss  6197  caoftrn  6199  ofsubge0  9835  pwsle  13490  pwsleval  13491  psrbaglesupp  16213  psrbagcon  16216  psrbaglefi  16217  psrlidm  16247  0plef  19131  0pledm  19132  itg1ge0  19145  mbfi1fseqlem5  19178  xrge0f  19190  itg2ge0  19194  itg2lea  19203  itg2splitlem  19207  itg2monolem1  19209  itg2mono  19212  itg2i1fseqle  19213  itg2i1fseq  19214  itg2addlem  19217  itg2cnlem1  19220  itg2addnclem  25492  itg2addnc  25494
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4212  ax-sep 4222  ax-nul 4230  ax-pr 4295
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-iun 3988  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-ofr 6166
  Copyright terms: Public domain W3C validator