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 = dom R
Assertion	istsr	|- ( R e. TosetRel <-> ( R e. PosetRel /\ ( X X. X ) C_ ( R u. `' R ) ) )

Proof

Step	Hyp	Ref	Expression
1		istsr.1	|- X = dom R
2		dmeq	|- ( r = R -> dom r = dom R )
3	2 1	eqtr4di	|- ( r = R -> dom r = X )
4	3	sqxpeqd	|- ( r = R -> ( dom r X. dom r ) = ( X X. X ) )
5		id	|- ( r = R -> r = R )
6		cnveq	|- ( r = R -> `' r = `' R )
7	5 6	uneq12d	|- ( r = R -> ( r u. `' r ) = ( R u. `' R ) )
8	4 7	sseq12d	|- ( r = R -> ( ( dom r X. dom r ) C_ ( r u. `' r ) <-> ( X X. X ) C_ ( R u. `' R ) ) )
9		df-tsr	|- TosetRel = { r e. PosetRel | ( dom r X. dom r ) C_ ( r u. `' r ) }
10	8 9	elrab2	|- ( R e. TosetRel <-> ( R e. PosetRel /\ ( X X. X ) C_ ( R u. `' R ) ) )