This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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