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