Theorem psssdm

Description: Field of a subposet. (Contributed by FL, 19-Sep-2011) (Revised by Mario Carneiro, 9-Sep-2015)

	Ref	Expression
Hypothesis	psssdm.1	$$⊢X=\mathrm{dom}R$$
Assertion	psssdm	$$⊢\left(R\in \mathrm{PosetRel}\wedge A\subseteq X\right)\to \mathrm{dom}\left(R\cap \left(A\times A\right)\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		psssdm.1	$$⊢X=\mathrm{dom}R$$
2	1	psssdm2	$$⊢R\in \mathrm{PosetRel}\to \mathrm{dom}\left(R\cap \left(A\times A\right)\right)=X\cap A$$
3		sseqin2	$$⊢A\subseteq X\leftrightarrow X\cap A=A$$
4	3	biimpi	$$⊢A\subseteq X\to X\cap A=A$$
5	2 4	sylan9eq	$$⊢\left(R\in \mathrm{PosetRel}\wedge A\subseteq X\right)\to \mathrm{dom}\left(R\cap \left(A\times A\right)\right)=A$$