Metamath Proof Explorer


Theorem cnvps

Description: The converse of a poset is a poset. In the general case (`' R e. PosetRel -> R e. PosetRel ) ` is not true. See cnvpsb for a special case where the property holds. (Contributed by FL, 5-Jan-2009) (Proof shortened by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion cnvps RPosetRelR-1PosetRel

Proof

Step Hyp Ref Expression
1 relcnv RelR-1
2 1 a1i RPosetRelRelR-1
3 cnvco RR-1=R-1R-1
4 pstr2 RPosetRelRRR
5 cnvss RRRRR-1R-1
6 4 5 syl RPosetRelRR-1R-1
7 3 6 eqsstrrid RPosetRelR-1R-1R-1
8 psrel RPosetRelRelR
9 dfrel2 RelRR-1-1=R
10 8 9 sylib RPosetRelR-1-1=R
11 10 ineq2d RPosetRelR-1R-1-1=R-1R
12 incom R-1R=RR-1
13 11 12 eqtrdi RPosetRelR-1R-1-1=RR-1
14 psref2 RPosetRelRR-1=IR
15 relcnvfld RelRR=R-1
16 8 15 syl RPosetRelR=R-1
17 16 reseq2d RPosetRelIR=IR-1
18 13 14 17 3eqtrd RPosetRelR-1R-1-1=IR-1
19 cnvexg RPosetRelR-1V
20 isps R-1VR-1PosetRelRelR-1R-1R-1R-1R-1R-1-1=IR-1
21 19 20 syl RPosetRelR-1PosetRelRelR-1R-1R-1R-1R-1R-1-1=IR-1
22 2 7 18 21 mpbir3and RPosetRelR-1PosetRel