This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsless

Description: Closure of the order relation on a structure product. (Contributed by Mario Carneiro, 16-Aug-2015)

Ref Expression
Hypotheses prdsbas.p 
|- P = ( S Xs_ R )
prdsbas.s 
|- ( ph -> S e. V )
prdsbas.r 
|- ( ph -> R e. W )
prdsbas.b 
|- B = ( Base ` P )
prdsbas.i 
|- ( ph -> dom R = I )
prdsle.l 
|- .<_ = ( le ` P )
Assertion prdsless 
|- ( ph -> .<_ C_ ( B X. B ) )

Proof

Step Hyp Ref Expression
1 prdsbas.p 
 |-  P = ( S Xs_ R )
2 prdsbas.s 
 |-  ( ph -> S e. V )
3 prdsbas.r 
 |-  ( ph -> R e. W )
4 prdsbas.b 
 |-  B = ( Base ` P )
5 prdsbas.i 
 |-  ( ph -> dom R = I )
6 prdsle.l 
 |-  .<_ = ( le ` P )
7 1 2 3 4 5 6 prdsle 
 |-  ( ph -> .<_ = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
8 vex 
 |-  f e. _V
9 vex 
 |-  g e. _V
10 8 9 prss 
 |-  ( ( f e. B /\ g e. B ) <-> { f , g } C_ B )
11 10 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 ) ) )
12 11 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 ) ) }
13 opabssxp 
 |-  { <. f , g >. | ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } C_ ( B X. B )
14 12 13 eqsstrri 
 |-  { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } C_ ( B X. B )
15 7 14 eqsstrdi 
 |-  ( ph -> .<_ C_ ( B X. B ) )