Theorem xpsless

Description: Closure of the ordering in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015)

	Ref	Expression
Hypotheses	xpsle.t	$$⊢T=R{\times }_{𝑠}S$$
	xpsle.x	$$⊢X={\mathrm{Base}}_R$$
	xpsle.y	$$⊢Y={\mathrm{Base}}_S$$
	xpsle.1	$$⊢\phi \to R\in V$$
	xpsle.2	$$⊢\phi \to S\in W$$
	xpsle.p	$$⊢\underset{\dot{}}{\le }={\le }_T$$
Assertion	xpsless	$$⊢\phi \to \underset{\dot{}}{\le }\subseteq \left(X\times Y\right)\times \left(X\times Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpsle.t	$$⊢T=R{\times }_{𝑠}S$$
2		xpsle.x	$$⊢X={\mathrm{Base}}_R$$
3		xpsle.y	$$⊢Y={\mathrm{Base}}_S$$
4		xpsle.1	$$⊢\phi \to R\in V$$
5		xpsle.2	$$⊢\phi \to S\in W$$
6		xpsle.p	$$⊢\underset{\dot{}}{\le }={\le }_T$$
7		eqid	$$⊢\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)=\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
8		eqid	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(R\right)$$
9		eqid	$$⊢\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}$$
10	1 2 3 4 5 7 8 9	xpsval	$$⊢\phi \to T={\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}{“}_{𝑠}\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)$$
11	1 2 3 4 5 7 8 9	xpsrnbas	$$⊢\phi \to \mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)={\mathrm{Base}}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)}$$
12	7	xpsff1o2	$$⊢\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right):X\times Y\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
13		f1ocnv	$$⊢\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right):X\times Y\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\to {\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{1-1\; onto}{⟶}X\times Y$$
14	12 13	mp1i	$$⊢\phi \to {\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{1-1\; onto}{⟶}X\times Y$$
15		f1ofo	$$⊢{\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{1-1\; onto}{⟶}X\times Y\to {\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{onto}{⟶}X\times Y$$
16	14 15	syl	$$⊢\phi \to {\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{onto}{⟶}X\times Y$$
17		ovexd	$$⊢\phi \to \mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\in \mathrm{V}$$
18	10 11 16 17 6	imasless	$$⊢\phi \to \underset{\dot{}}{\le }\subseteq \left(X\times Y\right)\times \left(X\times Y\right)$$