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

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

Metamath Proof Explorer