This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 )