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

Theorem ofrfval2 6337
Description: The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
offval2.1  |-  ( ph  ->  A  e.  V )
offval2.2  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  W )
offval2.3  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  X )
offval2.4  |-  ( ph  ->  F  =  ( x  e.  A  |->  B ) )
offval2.5  |-  ( ph  ->  G  =  ( x  e.  A  |->  C ) )
Assertion
Ref Expression
ofrfval2  |-  ( ph  ->  ( F  oR R G  <->  A. x  e.  A  B R C ) )
Distinct variable groups:    x, A    ph, x    x, R
Allowed substitution hints:    B( x)    C( x)    F( x)    G( x)    V( x)    W( x)    X( x)

Proof of Theorem ofrfval2
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 offval2.2 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  W )
21ralrimiva 2799 . . . . 5  |-  ( ph  ->  A. x  e.  A  B  e.  W )
3 eqid 2443 . . . . . 6  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
43fnmpt 5537 . . . . 5  |-  ( A. x  e.  A  B  e.  W  ->  ( x  e.  A  |->  B )  Fn  A )
52, 4syl 16 . . . 4  |-  ( ph  ->  ( x  e.  A  |->  B )  Fn  A
)
6 offval2.4 . . . . 5  |-  ( ph  ->  F  =  ( x  e.  A  |->  B ) )
76fneq1d 5501 . . . 4  |-  ( ph  ->  ( F  Fn  A  <->  ( x  e.  A  |->  B )  Fn  A ) )
85, 7mpbird 232 . . 3  |-  ( ph  ->  F  Fn  A )
9 offval2.3 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  X )
109ralrimiva 2799 . . . . 5  |-  ( ph  ->  A. x  e.  A  C  e.  X )
11 eqid 2443 . . . . . 6  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
1211fnmpt 5537 . . . . 5  |-  ( A. x  e.  A  C  e.  X  ->  ( x  e.  A  |->  C )  Fn  A )
1310, 12syl 16 . . . 4  |-  ( ph  ->  ( x  e.  A  |->  C )  Fn  A
)
14 offval2.5 . . . . 5  |-  ( ph  ->  G  =  ( x  e.  A  |->  C ) )
1514fneq1d 5501 . . . 4  |-  ( ph  ->  ( G  Fn  A  <->  ( x  e.  A  |->  C )  Fn  A ) )
1613, 15mpbird 232 . . 3  |-  ( ph  ->  G  Fn  A )
17 offval2.1 . . 3  |-  ( ph  ->  A  e.  V )
18 inidm 3559 . . 3  |-  ( A  i^i  A )  =  A
196adantr 465 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  F  =  ( x  e.  A  |->  B ) )
2019fveq1d 5693 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( F `  y )  =  ( ( x  e.  A  |->  B ) `
 y ) )
2114adantr 465 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  G  =  ( x  e.  A  |->  C ) )
2221fveq1d 5693 . . 3  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( ( x  e.  A  |->  C ) `
 y ) )
238, 16, 17, 17, 18, 20, 22ofrfval 6328 . 2  |-  ( ph  ->  ( F  oR R G  <->  A. y  e.  A  ( (
x  e.  A  |->  B ) `  y ) R ( ( x  e.  A  |->  C ) `
 y ) ) )
24 nffvmpt1 5699 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
25 nfcv 2579 . . . . 5  |-  F/_ x R
26 nffvmpt1 5699 . . . . 5  |-  F/_ x
( ( x  e.  A  |->  C ) `  y )
2724, 25, 26nfbr 4336 . . . 4  |-  F/ x
( ( x  e.  A  |->  B ) `  y ) R ( ( x  e.  A  |->  C ) `  y
)
28 nfv 1673 . . . 4  |-  F/ y ( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
)
29 fveq2 5691 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
30 fveq2 5691 . . . . 5  |-  ( y  =  x  ->  (
( x  e.  A  |->  C ) `  y
)  =  ( ( x  e.  A  |->  C ) `  x ) )
3129, 30breq12d 4305 . . . 4  |-  ( y  =  x  ->  (
( ( x  e.  A  |->  B ) `  y ) R ( ( x  e.  A  |->  C ) `  y
)  <->  ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x ) ) )
3227, 28, 31cbvral 2943 . . 3  |-  ( A. y  e.  A  (
( x  e.  A  |->  B ) `  y
) R ( ( x  e.  A  |->  C ) `  y )  <->  A. x  e.  A  ( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
) )
33 simpr 461 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
343fvmpt2 5781 . . . . . 6  |-  ( ( x  e.  A  /\  B  e.  W )  ->  ( ( x  e.  A  |->  B ) `  x )  =  B )
3533, 1, 34syl2anc 661 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  B ) `  x
)  =  B )
3611fvmpt2 5781 . . . . . 6  |-  ( ( x  e.  A  /\  C  e.  X )  ->  ( ( x  e.  A  |->  C ) `  x )  =  C )
3733, 9, 36syl2anc 661 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  C ) `  x
)  =  C )
3835, 37breq12d 4305 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( x  e.  A  |->  B ) `  x ) R ( ( x  e.  A  |->  C ) `  x
)  <->  B R C ) )
3938ralbidva 2731 . . 3  |-  ( ph  ->  ( A. x  e.  A  ( ( x  e.  A  |->  B ) `
 x ) R ( ( x  e.  A  |->  C ) `  x )  <->  A. x  e.  A  B R C ) )
4032, 39syl5bb 257 . 2  |-  ( ph  ->  ( A. y  e.  A  ( ( x  e.  A  |->  B ) `
 y ) R ( ( x  e.  A  |->  C ) `  y )  <->  A. x  e.  A  B R C ) )
4123, 40bitrd 253 1  |-  ( ph  ->  ( F  oR R G  <->  A. x  e.  A  B R C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2715   class class class wbr 4292    e. cmpt 4350    Fn wfn 5413   ` cfv 5418    oRcofr 6319
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-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531
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 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-ofr 6321
This theorem is referenced by:  gsumbagdiaglem  17445  mplmonmul  17543  coe1mul2lem1  17721  itg2const  21218  itg2const2  21219  itg2uba  21221  itg2mulclem  21224  itg2splitlem  21226  itg2split  21227  itg2monolem1  21228  itg2gt0  21238  itg2cnlem1  21239  itg2cnlem2  21240  iblss  21282  i1fibl  21285  itgitg1  21286  itgle  21287  ibladdlem  21297  iblabs  21306  iblabsr  21307  iblmulc2  21308  bddmulibl  21316  itg2addnclem  28443  itg2addnclem3  28445  itg2addnc  28446  itg2gt0cn  28447  ibladdnclem  28448  iblabsnc  28456  iblmulc2nc  28457  bddiblnc  28462  ftc1anclem4  28470  ftc1anclem5  28471  ftc1anclem6  28472  ftc1anclem7  28473  ftc1anclem8  28474  ftc1anc  28475
  Copyright terms: Public domain W3C validator