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 
|- ( R e. PosetRel -> `' R e. PosetRel )

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' R
2 1 a1i 
 |-  ( R e. PosetRel -> Rel `' R )
3 cnvco 
 |-  `' ( R o. R ) = ( `' R o. `' R )
4 pstr2 
 |-  ( R e. PosetRel -> ( R o. R ) C_ R )
5 cnvss 
 |-  ( ( R o. R ) C_ R -> `' ( R o. R ) C_ `' R )
6 4 5 syl 
 |-  ( R e. PosetRel -> `' ( R o. R ) C_ `' R )
7 3 6 eqsstrrid 
 |-  ( R e. PosetRel -> ( `' R o. `' R ) C_ `' R )
8 psrel 
 |-  ( R e. PosetRel -> Rel R )
9 dfrel2 
 |-  ( Rel R <-> `' `' R = R )
10 8 9 sylib 
 |-  ( R e. PosetRel -> `' `' R = R )
11 10 ineq2d 
 |-  ( R e. PosetRel -> ( `' R i^i `' `' R ) = ( `' R i^i R ) )
12 incom 
 |-  ( `' R i^i R ) = ( R i^i `' R )
13 11 12 eqtrdi 
 |-  ( R e. PosetRel -> ( `' R i^i `' `' R ) = ( R i^i `' R ) )
14 psref2 
 |-  ( R e. PosetRel -> ( R i^i `' R ) = ( _I |` U. U. R ) )
15 relcnvfld 
 |-  ( Rel R -> U. U. R = U. U. `' R )
16 8 15 syl 
 |-  ( R e. PosetRel -> U. U. R = U. U. `' R )
17 16 reseq2d 
 |-  ( R e. PosetRel -> ( _I |` U. U. R ) = ( _I |` U. U. `' R ) )
18 13 14 17 3eqtrd 
 |-  ( R e. PosetRel -> ( `' R i^i `' `' R ) = ( _I |` U. U. `' R ) )
19 cnvexg 
 |-  ( R e. PosetRel -> `' R e. _V )
20 isps 
 |-  ( `' R e. _V -> ( `' R e. PosetRel <-> ( Rel `' R /\ ( `' R o. `' R ) C_ `' R /\ ( `' R i^i `' `' R ) = ( _I |` U. U. `' R ) ) ) )
21 19 20 syl 
 |-  ( R e. PosetRel -> ( `' R e. PosetRel <-> ( Rel `' R /\ ( `' R o. `' R ) C_ `' R /\ ( `' R i^i `' `' R ) = ( _I |` U. U. `' R ) ) ) )
22 2 7 18 21 mpbir3and 
 |-  ( R e. PosetRel -> `' R e. PosetRel )