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

Metamath Proof Explorer

Theorem cnvpsb

Description: The converse of a poset is a poset. (Contributed by FL, 5-Jan-2009)

Ref Expression
Assertion cnvpsb 
|- ( Rel R -> ( R e. PosetRel <-> `' R e. PosetRel ) )

Proof

Step Hyp Ref Expression
1 cnvps 
 |-  ( R e. PosetRel -> `' R e. PosetRel )
2 cnvps 
 |-  ( `' R e. PosetRel -> `' `' R e. PosetRel )
3 dfrel2 
 |-  ( Rel R <-> `' `' R = R )
4 eleq1 
 |-  ( `' `' R = R -> ( `' `' R e. PosetRel <-> R e. PosetRel ) )
5 4 biimpd 
 |-  ( `' `' R = R -> ( `' `' R e. PosetRel -> R e. PosetRel ) )
6 3 5 sylbi 
 |-  ( Rel R -> ( `' `' R e. PosetRel -> R e. PosetRel ) )
7 2 6 syl5 
 |-  ( Rel R -> ( `' R e. PosetRel -> R e. PosetRel ) )
8 1 7 impbid2 
 |-  ( Rel R -> ( R e. PosetRel <-> `' R e. PosetRel ) )