Theorem istsr

Description: The predicate is a toset. (Contributed by FL, 1-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

	Ref	Expression
Hypothesis	istsr.1	$$⊢X=\mathrm{dom}R$$
Assertion	istsr	$$⊢R\in \mathrm{TosetRel}\leftrightarrow \left(R\in \mathrm{PosetRel}\wedge X\times X\subseteq R\cup R^{-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		istsr.1	$$⊢X=\mathrm{dom}R$$
2		dmeq	$$⊢r=R\to \mathrm{dom}r=\mathrm{dom}R$$
3	2 1	eqtr4di	$$⊢r=R\to \mathrm{dom}r=X$$
4	3	sqxpeqd	$$⊢r=R\to \mathrm{dom}r\times \mathrm{dom}r=X\times X$$
5		id	$$⊢r=R\to r=R$$
6		cnveq	$$⊢r=R\to r^{-1}=R^{-1}$$
7	5 6	uneq12d	$$⊢r=R\to r\cup r^{-1}=R\cup R^{-1}$$
8	4 7	sseq12d	$$⊢r=R\to \left(\mathrm{dom}r\times \mathrm{dom}r\subseteq r\cup r^{-1}\leftrightarrow X\times X\subseteq R\cup R^{-1}\right)$$
9		df-tsr	$$⊢\mathrm{TosetRel}=\left\{r\in \mathrm{PosetRel}|\mathrm{dom}r\times \mathrm{dom}r\subseteq r\cup r^{-1}\right\}$$
10	8 9	elrab2	$$⊢R\in \mathrm{TosetRel}\leftrightarrow \left(R\in \mathrm{PosetRel}\wedge X\times X\subseteq R\cup R^{-1}\right)$$