# 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}\mathrm{Po}{A}\to {{R}}^{-1}\mathrm{Po}{A}$

### Proof

Step Hyp Ref Expression
1 poirr ${⊢}\left({R}\mathrm{Po}{A}\wedge {x}\in {A}\right)\to ¬{x}{R}{x}$
2 vex ${⊢}{x}\in \mathrm{V}$
3 2 2 brcnv ${⊢}{x}{{R}}^{-1}{x}↔{x}{R}{x}$
4 1 3 sylnibr ${⊢}\left({R}\mathrm{Po}{A}\wedge {x}\in {A}\right)\to ¬{x}{{R}}^{-1}{x}$
5 3anrev ${⊢}\left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)↔\left({z}\in {A}\wedge {y}\in {A}\wedge {x}\in {A}\right)$
6 potr ${⊢}\left({R}\mathrm{Po}{A}\wedge \left({z}\in {A}\wedge {y}\in {A}\wedge {x}\in {A}\right)\right)\to \left(\left({z}{R}{y}\wedge {y}{R}{x}\right)\to {z}{R}{x}\right)$
7 5 6 sylan2b ${⊢}\left({R}\mathrm{Po}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to \left(\left({z}{R}{y}\wedge {y}{R}{x}\right)\to {z}{R}{x}\right)$
8 vex ${⊢}{y}\in \mathrm{V}$
9 2 8 brcnv ${⊢}{x}{{R}}^{-1}{y}↔{y}{R}{x}$
10 vex ${⊢}{z}\in \mathrm{V}$
11 8 10 brcnv ${⊢}{y}{{R}}^{-1}{z}↔{z}{R}{y}$
12 9 11 anbi12ci ${⊢}\left({x}{{R}}^{-1}{y}\wedge {y}{{R}}^{-1}{z}\right)↔\left({z}{R}{y}\wedge {y}{R}{x}\right)$
13 2 10 brcnv ${⊢}{x}{{R}}^{-1}{z}↔{z}{R}{x}$
14 7 12 13 3imtr4g ${⊢}\left({R}\mathrm{Po}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to \left(\left({x}{{R}}^{-1}{y}\wedge {y}{{R}}^{-1}{z}\right)\to {x}{{R}}^{-1}{z}\right)$
15 4 14 ispod ${⊢}{R}\mathrm{Po}{A}\to {{R}}^{-1}\mathrm{Po}{A}$