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 ( 𝑅 Po 𝐴 𝑅 Po 𝐴 )

Proof

Step Hyp Ref Expression
1 poirr ( ( 𝑅 Po 𝐴𝑥𝐴 ) → ¬ 𝑥 𝑅 𝑥 )
2 vex 𝑥 ∈ V
3 2 2 brcnv ( 𝑥 𝑅 𝑥𝑥 𝑅 𝑥 )
4 1 3 sylnibr ( ( 𝑅 Po 𝐴𝑥𝐴 ) → ¬ 𝑥 𝑅 𝑥 )
5 3anrev ( ( 𝑥𝐴𝑦𝐴𝑧𝐴 ) ↔ ( 𝑧𝐴𝑦𝐴𝑥𝐴 ) )
6 potr ( ( 𝑅 Po 𝐴 ∧ ( 𝑧𝐴𝑦𝐴𝑥𝐴 ) ) → ( ( 𝑧 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑧 𝑅 𝑥 ) )
7 5 6 sylan2b ( ( 𝑅 Po 𝐴 ∧ ( 𝑥𝐴𝑦𝐴𝑧𝐴 ) ) → ( ( 𝑧 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑧 𝑅 𝑥 ) )
8 vex 𝑦 ∈ V
9 2 8 brcnv ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 )
10 vex 𝑧 ∈ V
11 8 10 brcnv ( 𝑦 𝑅 𝑧𝑧 𝑅 𝑦 )
12 9 11 anbi12ci ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑧 ) ↔ ( 𝑧 𝑅 𝑦𝑦 𝑅 𝑥 ) )
13 2 10 brcnv ( 𝑥 𝑅 𝑧𝑧 𝑅 𝑥 )
14 7 12 13 3imtr4g ( ( 𝑅 Po 𝐴 ∧ ( 𝑥𝐴𝑦𝐴𝑧𝐴 ) ) → ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
15 4 14 ispod ( 𝑅 Po 𝐴 𝑅 Po 𝐴 )