Theorem psssdm2

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

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

Proof

Step	Hyp	Ref	Expression
1		psssdm.1	$$⊢X=\mathrm{dom}R$$
2		dmin	$$⊢\mathrm{dom}\left(R\cap \left(A\times A\right)\right)\subseteq \mathrm{dom}R\cap \mathrm{dom}\left(A\times A\right)$$
3	1	eqcomi	$$⊢\mathrm{dom}R=X$$
4		dmxpid	$$⊢\mathrm{dom}\left(A\times A\right)=A$$
5	3 4	ineq12i	$$⊢\mathrm{dom}R\cap \mathrm{dom}\left(A\times A\right)=X\cap A$$
6	2 5	sseqtri	$$⊢\mathrm{dom}\left(R\cap \left(A\times A\right)\right)\subseteq X\cap A$$
7	6	a1i	$$⊢R\in \mathrm{PosetRel}\to \mathrm{dom}\left(R\cap \left(A\times A\right)\right)\subseteq X\cap A$$
8		simpr	$$⊢\left(R\in \mathrm{PosetRel}\wedge x\in \left(X\cap A\right)\right)\to x\in \left(X\cap A\right)$$
9	8	elin2d	$$⊢\left(R\in \mathrm{PosetRel}\wedge x\in \left(X\cap A\right)\right)\to x\in A$$
10		elinel1	$$⊢x\in \left(X\cap A\right)\to x\in X$$
11	1	psref	$$⊢\left(R\in \mathrm{PosetRel}\wedge x\in X\right)\to xRx$$
12	10 11	sylan2	$$⊢\left(R\in \mathrm{PosetRel}\wedge x\in \left(X\cap A\right)\right)\to xRx$$
13		brinxp2	$$⊢x\left(R\cap \left(A\times A\right)\right)x\leftrightarrow \left(\left(x\in A\wedge x\in A\right)\wedge xRx\right)$$
14	9 9 12 13	syl21anbrc	$$⊢\left(R\in \mathrm{PosetRel}\wedge x\in \left(X\cap A\right)\right)\to x\left(R\cap \left(A\times A\right)\right)x$$
15		vex	$$⊢x\in \mathrm{V}$$
16	15 15	breldm	$$⊢x\left(R\cap \left(A\times A\right)\right)x\to x\in \mathrm{dom}\left(R\cap \left(A\times A\right)\right)$$
17	14 16	syl	$$⊢\left(R\in \mathrm{PosetRel}\wedge x\in \left(X\cap A\right)\right)\to x\in \mathrm{dom}\left(R\cap \left(A\times A\right)\right)$$
18	7 17	eqelssd	$$⊢R\in \mathrm{PosetRel}\to \mathrm{dom}\left(R\cap \left(A\times A\right)\right)=X\cap A$$