cnvpo

Description: The converse of a partial order relation is a partial order relation. (Contributed by NM, 15-Jun-2005)

		Ref	Expression
	Assertion	cnvpo	$⊢ R Po A \leftrightarrow R^{-1} Po A$

Proof

Step	Hyp	Ref	Expression
1		r19.26	$⊢ \forall z \in A (\neg z R^{-1} z \land ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x)) \leftrightarrow (\forall z \in A \neg z R^{-1} z \land \forall z \in A ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x))$
2		vex	$⊢ z \in V$
3	2 2	brcnv	$⊢ z R^{-1} z \leftrightarrow z R z$
4		id	$⊢ z = x \to z = x$
5	4 4	breq12d	$⊢ z = x \to (z R z \leftrightarrow x R x)$
6	3 5	syl5bb	$⊢ z = x \to (z R^{-1} z \leftrightarrow x R x)$
7	6	notbid	$⊢ z = x \to (\neg z R^{-1} z \leftrightarrow \neg x R x)$
8	7	cbvralvw	$⊢ \forall z \in A \neg z R^{-1} z \leftrightarrow \forall x \in A \neg x R x$
9		vex	$⊢ y \in V$
10	2 9	brcnv	$⊢ z R^{-1} y \leftrightarrow y R z$
11		vex	$⊢ x \in V$
12	9 11	brcnv	$⊢ y R^{-1} x \leftrightarrow x R y$
13	10 12	anbi12ci	$⊢ (z R^{-1} y \land y R^{-1} x) \leftrightarrow (x R y \land y R z)$
14	2 11	brcnv	$⊢ z R^{-1} x \leftrightarrow x R z$
15	13 14	imbi12i	$⊢ ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x) \leftrightarrow ((x R y \land y R z) \to x R z)$
16	15	ralbii	$⊢ \forall z \in A ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x) \leftrightarrow \forall z \in A ((x R y \land y R z) \to x R z)$
17	8 16	anbi12i	$⊢ (\forall z \in A \neg z R^{-1} z \land \forall z \in A ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x)) \leftrightarrow (\forall x \in A \neg x R x \land \forall z \in A ((x R y \land y R z) \to x R z))$
18	1 17	bitr2i	$⊢ (\forall x \in A \neg x R x \land \forall z \in A ((x R y \land y R z) \to x R z)) \leftrightarrow \forall z \in A (\neg z R^{-1} z \land ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x))$
19	18	ralbii	$⊢ \forall x \in A (\forall x \in A \neg x R x \land \forall z \in A ((x R y \land y R z) \to x R z)) \leftrightarrow \forall x \in A \forall z \in A (\neg z R^{-1} z \land ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x))$
20		r19.26	$⊢ \forall x \in A (\forall z \in A \neg x R x \land \forall z \in A ((x R y \land y R z) \to x R z)) \leftrightarrow (\forall x \in A \forall z \in A \neg x R x \land \forall x \in A \forall z \in A ((x R y \land y R z) \to x R z))$
21		ralidm	$⊢ \forall x \in A \forall x \in A \neg x R x \leftrightarrow \forall x \in A \neg x R x$
22		rzal	$⊢ A = \emptyset \to \forall x \in A \neg x R x$
23		rzal	$⊢ A = \emptyset \to \forall x \in A \forall z \in A \neg x R x$
24	22 23	2thd	$⊢ A = \emptyset \to (\forall x \in A \neg x R x \leftrightarrow \forall x \in A \forall z \in A \neg x R x)$
25		r19.3rzv	$⊢ A \neq \emptyset \to (\neg x R x \leftrightarrow \forall z \in A \neg x R x)$
26	25	ralbidv	$⊢ A \neq \emptyset \to (\forall x \in A \neg x R x \leftrightarrow \forall x \in A \forall z \in A \neg x R x)$
27	24 26	pm2.61ine	$⊢ \forall x \in A \neg x R x \leftrightarrow \forall x \in A \forall z \in A \neg x R x$
28	21 27	bitr2i	$⊢ \forall x \in A \forall z \in A \neg x R x \leftrightarrow \forall x \in A \forall x \in A \neg x R x$
29	28	anbi1i	$⊢ (\forall x \in A \forall z \in A \neg x R x \land \forall x \in A \forall z \in A ((x R y \land y R z) \to x R z)) \leftrightarrow (\forall x \in A \forall x \in A \neg x R x \land \forall x \in A \forall z \in A ((x R y \land y R z) \to x R z))$
30	20 29	bitri	$⊢ \forall x \in A (\forall z \in A \neg x R x \land \forall z \in A ((x R y \land y R z) \to x R z)) \leftrightarrow (\forall x \in A \forall x \in A \neg x R x \land \forall x \in A \forall z \in A ((x R y \land y R z) \to x R z))$
31		r19.26	$⊢ \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow (\forall z \in A \neg x R x \land \forall z \in A ((x R y \land y R z) \to x R z))$
32	31	ralbii	$⊢ \forall x \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall x \in A (\forall z \in A \neg x R x \land \forall z \in A ((x R y \land y R z) \to x R z))$
33		r19.26	$⊢ \forall x \in A (\forall x \in A \neg x R x \land \forall z \in A ((x R y \land y R z) \to x R z)) \leftrightarrow (\forall x \in A \forall x \in A \neg x R x \land \forall x \in A \forall z \in A ((x R y \land y R z) \to x R z))$
34	30 32 33	3bitr4i	$⊢ \forall x \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall x \in A (\forall x \in A \neg x R x \land \forall z \in A ((x R y \land y R z) \to x R z))$
35		ralcom	$⊢ \forall z \in A \forall x \in A (\neg z R^{-1} z \land ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x)) \leftrightarrow \forall x \in A \forall z \in A (\neg z R^{-1} z \land ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x))$
36	19 34 35	3bitr4i	$⊢ \forall x \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall z \in A \forall x \in A (\neg z R^{-1} z \land ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x))$
37	36	ralbii	$⊢ \forall y \in A \forall x \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall y \in A \forall z \in A \forall x \in A (\neg z R^{-1} z \land ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x))$
38		ralcom	$⊢ \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall y \in A \forall x \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z))$
39		ralcom	$⊢ \forall z \in A \forall y \in A \forall x \in A (\neg z R^{-1} z \land ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x)) \leftrightarrow \forall y \in A \forall z \in A \forall x \in A (\neg z R^{-1} z \land ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x))$
40	37 38 39	3bitr4i	$⊢ \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall z \in A \forall y \in A \forall x \in A (\neg z R^{-1} z \land ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x))$
41		df-po	$⊢ R Po A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z))$
42		df-po	$⊢ R^{-1} Po A \leftrightarrow \forall z \in A \forall y \in A \forall x \in A (\neg z R^{-1} z \land ((z R^{-1} y \land y R^{-1} x) \to z R^{-1} x))$
43	40 41 42	3bitr4i	$⊢ R Po A \leftrightarrow R^{-1} Po A$

Metamath Proof Explorer

Theorem cnvpo

Proof