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