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