Metamath Proof Explorer

Theorem pwsleval

Description: Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015)

Ref Expression
Hypotheses pwsle.y 
|- Y = ( R ^s I )
pwsle.v 
|- B = ( Base ` Y )
pwsle.o 
|- O = ( le ` R )
pwsle.l 
|- .<_ = ( le ` Y )
pwsleval.r 
|- ( ph -> R e. V )
pwsleval.i 
|- ( ph -> I e. W )
pwsleval.a 
|- ( ph -> F e. B )
pwsleval.b 
|- ( ph -> G e. B )
Assertion pwsleval 
|- ( ph -> ( F .<_ G <-> A. x e. I ( F ` x ) O ( G ` x ) ) )

Proof

Step Hyp Ref Expression
1 pwsle.y 
 |-  Y = ( R ^s I )
2 pwsle.v 
 |-  B = ( Base ` Y )
3 pwsle.o 
 |-  O = ( le ` R )
4 pwsle.l 
 |-  .<_ = ( le ` Y )
5 pwsleval.r 
 |-  ( ph -> R e. V )
6 pwsleval.i 
 |-  ( ph -> I e. W )
7 pwsleval.a 
 |-  ( ph -> F e. B )
8 pwsleval.b 
 |-  ( ph -> G e. B )
9 1 2 3 4 pwsle 
 |-  ( ( R e. V /\ I e. W ) -> .<_ = ( oR O i^i ( B X. B ) ) )
10 5 6 9 syl2anc 
 |-  ( ph -> .<_ = ( oR O i^i ( B X. B ) ) )
11 10 breqd 
 |-  ( ph -> ( F .<_ G <-> F ( oR O i^i ( B X. B ) ) G ) )
12 brinxp 
 |-  ( ( F e. B /\ G e. B ) -> ( F oR O G <-> F ( oR O i^i ( B X. B ) ) G ) )
13 7 8 12 syl2anc 
 |-  ( ph -> ( F oR O G <-> F ( oR O i^i ( B X. B ) ) G ) )
14 eqid 
 |-  ( Base ` R ) = ( Base ` R )
15 1 14 2 5 6 7 pwselbas 
 |-  ( ph -> F : I --> ( Base ` R ) )
16 15 ffnd 
 |-  ( ph -> F Fn I )
17 1 14 2 5 6 8 pwselbas 
 |-  ( ph -> G : I --> ( Base ` R ) )
18 17 ffnd 
 |-  ( ph -> G Fn I )
19 inidm 
 |-  ( I i^i I ) = I
20 eqidd 
 |-  ( ( ph /\ x e. I ) -> ( F ` x ) = ( F ` x ) )
21 eqidd 
 |-  ( ( ph /\ x e. I ) -> ( G ` x ) = ( G ` x ) )
22 16 18 7 8 19 20 21 ofrfvalg 
 |-  ( ph -> ( F oR O G <-> A. x e. I ( F ` x ) O ( G ` x ) ) )
23 11 13 22 3bitr2d 
 |-  ( ph -> ( F .<_ G <-> A. x e. I ( F ` x ) O ( G ` x ) ) )