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