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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv | |
|
2 | 1 | a1i | |
3 | cnvco | |
|
4 | pstr2 | |
|
5 | cnvss | |
|
6 | 4 5 | syl | |
7 | 3 6 | eqsstrrid | |
8 | psrel | |
|
9 | dfrel2 | |
|
10 | 8 9 | sylib | |
11 | 10 | ineq2d | |
12 | incom | |
|
13 | 11 12 | eqtrdi | |
14 | psref2 | |
|
15 | relcnvfld | |
|
16 | 8 15 | syl | |
17 | 16 | reseq2d | |
18 | 13 14 17 | 3eqtrd | |
19 | cnvexg | |
|
20 | isps | |
|
21 | 19 20 | syl | |
22 | 2 7 18 21 | mpbir3and | |