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 )