Metamath Proof Explorer

Theorem istsr2

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 istsr2 
|- ( R e. TosetRel <-> ( R e. PosetRel /\ A. x e. X A. y e. X ( x R y \/ y R x ) ) )

Proof

Step Hyp Ref Expression
1 istsr.1 
 |-  X = dom R
2 1 istsr 
 |-  ( R e. TosetRel <-> ( R e. PosetRel /\ ( X X. X ) C_ ( R u. `' R ) ) )
3 qfto 
 |-  ( ( X X. X ) C_ ( R u. `' R ) <-> A. x e. X A. y e. X ( x R y \/ y R x ) )
4 3 anbi2i 
 |-  ( ( R e. PosetRel /\ ( X X. X ) C_ ( R u. `' R ) ) <-> ( R e. PosetRel /\ A. x e. X A. y e. X ( x R y \/ y R x ) ) )
5 2 4 bitri 
 |-  ( R e. TosetRel <-> ( R e. PosetRel /\ A. x e. X A. y e. X ( x R y \/ y R x ) ) )