Metamath Proof Explorer


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 ) ) )