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 ) ) )