Metamath Proof Explorer

Theorem psref2

Description: A poset is antisymmetric and reflexive. (Contributed by FL, 3-Aug-2009)

Ref Expression
Assertion psref2 
|- ( R e. PosetRel -> ( R i^i `' R ) = ( _I |` U. U. R ) )

Proof

Step Hyp Ref Expression
1 isps 
 |-  ( R e. PosetRel -> ( R e. PosetRel <-> ( Rel R /\ ( R o. R ) C_ R /\ ( R i^i `' R ) = ( _I |` U. U. R ) ) ) )
2 1 ibi 
 |-  ( R e. PosetRel -> ( Rel R /\ ( R o. R ) C_ R /\ ( R i^i `' R ) = ( _I |` U. U. R ) ) )
3 2 simp3d 
 |-  ( R e. PosetRel -> ( R i^i `' R ) = ( _I |` U. U. R ) )