Metamath Proof Explorer

Theorem prdsleval

Description: Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypotheses prdsbasmpt.y 
|- Y = ( S Xs_ R )
prdsbasmpt.b 
|- B = ( Base ` Y )
prdsbasmpt.s 
|- ( ph -> S e. V )
prdsbasmpt.i 
|- ( ph -> I e. W )
prdsbasmpt.r 
|- ( ph -> R Fn I )
prdsplusgval.f 
|- ( ph -> F e. B )
prdsplusgval.g 
|- ( ph -> G e. B )
prdsleval.l 
|- .<_ = ( le ` Y )
Assertion prdsleval 
|- ( ph -> ( F .<_ G <-> A. x e. I ( F ` x ) ( le ` ( R ` x ) ) ( G ` x ) ) )

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y 
 |-  Y = ( S Xs_ R )
2 prdsbasmpt.b 
 |-  B = ( Base ` Y )
3 prdsbasmpt.s 
 |-  ( ph -> S e. V )
4 prdsbasmpt.i 
 |-  ( ph -> I e. W )
5 prdsbasmpt.r 
 |-  ( ph -> R Fn I )
6 prdsplusgval.f 
 |-  ( ph -> F e. B )
7 prdsplusgval.g 
 |-  ( ph -> G e. B )
8 prdsleval.l 
 |-  .<_ = ( le ` Y )
9 df-br 
 |-  ( F .<_ G <-> <. F , G >. e. .<_ )
10 fnex 
 |-  ( ( R Fn I /\ I e. W ) -> R e. _V )
11 5 4 10 syl2anc 
 |-  ( ph -> R e. _V )
12 5 fndmd 
 |-  ( ph -> dom R = I )
13 1 3 11 2 12 8 prdsle 
 |-  ( ph -> .<_ = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
14 vex 
 |-  f e. _V
15 vex 
 |-  g e. _V
16 14 15 prss 
 |-  ( ( f e. B /\ g e. B ) <-> { f , g } C_ B )
17 16 anbi1i 
 |-  ( ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) <-> ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) )
18 17 opabbii 
 |-  { <. f , g >. | ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) }
19 13 18 eqtr4di 
 |-  ( ph -> .<_ = { <. f , g >. | ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
20 19 eleq2d 
 |-  ( ph -> ( <. F , G >. e. .<_ <-> <. F , G >. e. { <. f , g >. | ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } ) )
21 9 20 bitrid 
 |-  ( ph -> ( F .<_ G <-> <. F , G >. e. { <. f , g >. | ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } ) )
22 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
23 fveq1 
 |-  ( g = G -> ( g ` x ) = ( G ` x ) )
24 22 23 breqan12d 
 |-  ( ( f = F /\ g = G ) -> ( ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) <-> ( F ` x ) ( le ` ( R ` x ) ) ( G ` x ) ) )
25 24 ralbidv 
 |-  ( ( f = F /\ g = G ) -> ( A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) <-> A. x e. I ( F ` x ) ( le ` ( R ` x ) ) ( G ` x ) ) )
26 25 opelopab2a 
 |-  ( ( F e. B /\ G e. B ) -> ( <. F , G >. e. { <. f , g >. | ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } <-> A. x e. I ( F ` x ) ( le ` ( R ` x ) ) ( G ` x ) ) )
27 6 7 26 syl2anc 
 |-  ( ph -> ( <. F , G >. e. { <. f , g >. | ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } <-> A. x e. I ( F ` x ) ( le ` ( R ` x ) ) ( G ` x ) ) )
28 21 27 bitrd 
 |-  ( ph -> ( F .<_ G <-> A. x e. I ( F ` x ) ( le ` ( R ` x ) ) ( G ` x ) ) )