Theorem prsssdm

Description: Domain of a subproset relation. (Contributed by Thierry Arnoux, 12-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	prsssdm	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=A$$

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	1 2	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)$$
4	3	dmeqd	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=\mathrm{dom}\left({\le }_K\cap \left(A\times A\right)\right)$$
5	1	ressprs	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to K{\upharpoonright }_{𝑠}A\in \mathrm{Proset}$$
6		eqid	$$⊢{\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
7		eqid	$$⊢{\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)={\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)$$
8	6 7	prsdm	$$⊢K{\upharpoonright }_{𝑠}A\in \mathrm{Proset}\to \mathrm{dom}\left({\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)\right)={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
9	5 8	syl	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to \mathrm{dom}\left({\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)\right)={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
10		eqid	$$⊢K{\upharpoonright }_{𝑠}A=K{\upharpoonright }_{𝑠}A$$
11	10 1	ressbas2	$$⊢A\subseteq B\to A={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
12		fvex	$$⊢{\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\in \mathrm{V}$$
13	11 12	eqeltrdi	$$⊢A\subseteq B\to A\in \mathrm{V}$$
14		eqid	$$⊢{\le }_K={\le }_K$$
15	10 14	ressle	$$⊢A\in \mathrm{V}\to {\le }_K={\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
16	13 15	syl	$$⊢A\subseteq B\to {\le }_K={\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
17	16	adantl	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to {\le }_K={\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
18	11	adantl	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to A={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
19	18	sqxpeqd	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to A\times A={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
20	17 19	ineq12d	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to {\le }_K\cap \left(A\times A\right)={\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)$$
21	20	dmeqd	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to \mathrm{dom}\left({\le }_K\cap \left(A\times A\right)\right)=\mathrm{dom}\left({\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)\right)$$
22	9 21 18	3eqtr4d	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to \mathrm{dom}\left({\le }_K\cap \left(A\times A\right)\right)=A$$
23	4 22	eqtrd	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=A$$