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