# Metamath Proof Explorer

## Theorem pocnv

Description: The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018)

Ref Expression
Assertion pocnv
`|- ( R Po A -> `' R Po A )`

### Proof

Step Hyp Ref Expression
1 poirr
` |-  ( ( R Po A /\ x e. A ) -> -. x R x )`
2 vex
` |-  x e. _V`
3 2 2 brcnv
` |-  ( x `' R x <-> x R x )`
4 1 3 sylnibr
` |-  ( ( R Po A /\ x e. A ) -> -. x `' R x )`
5 3anrev
` |-  ( ( x e. A /\ y e. A /\ z e. A ) <-> ( z e. A /\ y e. A /\ x e. A ) )`
6 potr
` |-  ( ( R Po A /\ ( z e. A /\ y e. A /\ x e. A ) ) -> ( ( z R y /\ y R x ) -> z R x ) )`
7 5 6 sylan2b
` |-  ( ( R Po A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( z R y /\ y R x ) -> z R x ) )`
8 vex
` |-  y e. _V`
9 2 8 brcnv
` |-  ( x `' R y <-> y R x )`
10 vex
` |-  z e. _V`
11 8 10 brcnv
` |-  ( y `' R z <-> z R y )`
12 9 11 anbi12ci
` |-  ( ( x `' R y /\ y `' R z ) <-> ( z R y /\ y R x ) )`
13 2 10 brcnv
` |-  ( x `' R z <-> z R x )`
14 7 12 13 3imtr4g
` |-  ( ( R Po A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x `' R y /\ y `' R z ) -> x `' R z ) )`
15 4 14 ispod
` |-  ( R Po A -> `' R Po A )`