Theorem prsss

Description: Relation of a subproset. (Contributed by Thierry Arnoux, 13-Sep-2018)

	Ref	Expression
Hypotheses	ordtNEW.b	$$⊢B={\mathrm{Base}}_K$$
	ordtNEW.l	$$⊢\underset{\dot{}}{\le }={\le }_K\cap \left(B\times B\right)$$
Assertion	prsss	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to \underset{\dot{}}{\le }\cap \left(A\times A\right)={\le }_K\cap \left(A\times A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ordtNEW.b	$$⊢B={\mathrm{Base}}_K$$
2		ordtNEW.l	$$⊢\underset{\dot{}}{\le }={\le }_K\cap \left(B\times B\right)$$
3	2	ineq1i	$$⊢\underset{\dot{}}{\le }\cap \left(A\times A\right)=\left({\le }_K\cap \left(B\times B\right)\right)\cap \left(A\times A\right)$$
4		inass	$$⊢\left({\le }_K\cap \left(B\times B\right)\right)\cap \left(A\times A\right)={\le }_K\cap \left(\left(B\times B\right)\cap \left(A\times A\right)\right)$$
5	3 4	eqtri	$$⊢\underset{\dot{}}{\le }\cap \left(A\times A\right)={\le }_K\cap \left(\left(B\times B\right)\cap \left(A\times A\right)\right)$$
6		xpss12	$$⊢\left(A\subseteq B\wedge A\subseteq B\right)\to A\times A\subseteq B\times B$$
7	6	anidms	$$⊢A\subseteq B\to A\times A\subseteq B\times B$$
8		sseqin2	$$⊢A\times A\subseteq B\times B\leftrightarrow \left(B\times B\right)\cap \left(A\times A\right)=A\times A$$
9	7 8	sylib	$$⊢A\subseteq B\to \left(B\times B\right)\cap \left(A\times A\right)=A\times A$$
10	9	ineq2d	$$⊢A\subseteq B\to {\le }_K\cap \left(\left(B\times B\right)\cap \left(A\times A\right)\right)={\le }_K\cap \left(A\times A\right)$$
11	5 10	syl5eq	$$⊢A\subseteq B\to \underset{\dot{}}{\le }\cap \left(A\times A\right)={\le }_K\cap \left(A\times A\right)$$
12	11	adantl	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to \underset{\dot{}}{\le }\cap \left(A\times A\right)={\le }_K\cap \left(A\times A\right)$$