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 ∈ PosetRel ↔ R -1 ∈ PosetRel

Proof

Step Hyp Ref Expression
1 cnvps ⊢ R ∈ PosetRel → R -1 ∈ PosetRel
2 cnvps ⊢ R -1 ∈ PosetRel → R -1 -1 ∈ PosetRel
3 dfrel2 ⊢ Rel ⁡ R ↔ R -1 -1 = R
4 eleq1 ⊢ R -1 -1 = R → R -1 -1 ∈ PosetRel ↔ R ∈ PosetRel
5 4 biimpd ⊢ R -1 -1 = R → R -1 -1 ∈ PosetRel → R ∈ PosetRel
6 3 5 sylbi ⊢ Rel ⁡ R → R -1 -1 ∈ PosetRel → R ∈ PosetRel
7 2 6 syl5 ⊢ Rel ⁡ R → R -1 ∈ PosetRel → R ∈ PosetRel
8 1 7 impbid2 ⊢ Rel ⁡ R → R ∈ PosetRel ↔ R -1 ∈ PosetRel