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 = dom R$
	Assertion	istsr	$⊢ R \in TosetRel \leftrightarrow (R \in PosetRel \land X \times X \subseteq R \cup R^{-1})$

Step	Hyp	Ref	Expression
1		istsr.1	$⊢ X = dom R$
2		dmeq	$⊢ r = R \to dom r = dom R$
3	2 1	eqtr4di	$⊢ r = R \to dom r = X$
4	3	sqxpeqd	$⊢ r = R \to dom r \times 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 (dom r \times dom r \subseteq r \cup r^{-1} \leftrightarrow X \times X \subseteq R \cup R^{-1})$
9		df-tsr	$⊢ TosetRel = \{r \in PosetRel \| dom r \times dom r \subseteq r \cup r^{-1}\}$
10	8 9	elrab2	$⊢ R \in TosetRel \leftrightarrow (R \in PosetRel \land X \times X \subseteq R \cup R^{-1})$

Metamath Proof Explorer