dfpo2

Description: Quantifier-free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013) (Proof shortened by Peter Mazsa, 2-Oct-2022)

		Ref	Expression
	Assertion	dfpo2	$⊢ R Po A \leftrightarrow (R \cap ({I ↾}_{A}) = \emptyset \land (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R)$

Proof

Step	Hyp	Ref	Expression
1		po0	$⊢ R Po \emptyset$
2		res0	$⊢ {I ↾}_{\emptyset} = \emptyset$
3	2	ineq2i	$⊢ R \cap ({I ↾}_{\emptyset}) = R \cap \emptyset$
4		in0	$⊢ R \cap \emptyset = \emptyset$
5	3 4	eqtri	$⊢ R \cap ({I ↾}_{\emptyset}) = \emptyset$
6		xp0	$⊢ A \times \emptyset = \emptyset$
7	6	ineq2i	$⊢ R \cap (A \times \emptyset) = R \cap \emptyset$
8	7 4	eqtri	$⊢ R \cap (A \times \emptyset) = \emptyset$
9	8	coeq2i	$⊢ (R \cap (A \times A)) \circ (R \cap (A \times \emptyset)) = (R \cap (A \times A)) \circ \emptyset$
10		co02	$⊢ (R \cap (A \times A)) \circ \emptyset = \emptyset$
11	9 10	eqtri	$⊢ (R \cap (A \times A)) \circ (R \cap (A \times \emptyset)) = \emptyset$
12		0ss	$⊢ \emptyset \subseteq R$
13	11 12	eqsstri	$⊢ (R \cap (A \times A)) \circ (R \cap (A \times \emptyset)) \subseteq R$
14	5 13	pm3.2i	$⊢ (R \cap ({I ↾}_{\emptyset}) = \emptyset \land (R \cap (A \times A)) \circ (R \cap (A \times \emptyset)) \subseteq R)$
15	1 14	2th	$⊢ R Po \emptyset \leftrightarrow (R \cap ({I ↾}_{\emptyset}) = \emptyset \land (R \cap (A \times A)) \circ (R \cap (A \times \emptyset)) \subseteq R)$
16		poeq2	$⊢ A = \emptyset \to (R Po A \leftrightarrow R Po \emptyset)$
17		reseq2	$⊢ A = \emptyset \to {I ↾}_{A} = {I ↾}_{\emptyset}$
18	17	ineq2d	$⊢ A = \emptyset \to R \cap ({I ↾}_{A}) = R \cap ({I ↾}_{\emptyset})$
19	18	eqeq1d	$⊢ A = \emptyset \to (R \cap ({I ↾}_{A}) = \emptyset \leftrightarrow R \cap ({I ↾}_{\emptyset}) = \emptyset)$
20		xpeq2	$⊢ A = \emptyset \to A \times A = A \times \emptyset$
21	20	ineq2d	$⊢ A = \emptyset \to R \cap (A \times A) = R \cap (A \times \emptyset)$
22	21	coeq2d	$⊢ A = \emptyset \to (R \cap (A \times A)) \circ (R \cap (A \times A)) = (R \cap (A \times A)) \circ (R \cap (A \times \emptyset))$
23	22	sseq1d	$⊢ A = \emptyset \to ((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \leftrightarrow (R \cap (A \times A)) \circ (R \cap (A \times \emptyset)) \subseteq R)$
24	19 23	anbi12d	$⊢ A = \emptyset \to ((R \cap ({I ↾}_{A}) = \emptyset \land (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R) \leftrightarrow (R \cap ({I ↾}_{\emptyset}) = \emptyset \land (R \cap (A \times A)) \circ (R \cap (A \times \emptyset)) \subseteq R))$
25	16 24	bibi12d	$⊢ A = \emptyset \to ((R Po A \leftrightarrow (R \cap ({I ↾}_{A}) = \emptyset \land (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R)) \leftrightarrow (R Po \emptyset \leftrightarrow (R \cap ({I ↾}_{\emptyset}) = \emptyset \land (R \cap (A \times A)) \circ (R \cap (A \times \emptyset)) \subseteq R)))$
26	15 25	mpbiri	$⊢ A = \emptyset \to (R Po A \leftrightarrow (R \cap ({I ↾}_{A}) = \emptyset \land (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R))$
27		r19.28zv	$⊢ A \neq \emptyset \to (\forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow (\neg x R x \land \forall z \in A ((x R y \land y R z) \to x R z)))$
28	27	ralbidv	$⊢ A \neq \emptyset \to (\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 (\neg x R x \land \forall z \in A ((x R y \land y R z) \to x R z)))$
29		r19.28zv	$⊢ A \neq \emptyset \to (\forall y \in A (\neg x R x \land \forall z \in A ((x R y \land y R z) \to x R z)) \leftrightarrow (\neg x R x \land \forall y \in A \forall z \in A ((x R y \land y R z) \to x R z)))$
30	28 29	bitrd	$⊢ A \neq \emptyset \to (\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 (\neg x R x \land \forall y \in A \forall z \in A ((x R y \land y R z) \to x R z)))$
31	30	ralbidv	$⊢ A \neq \emptyset \to (\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 x \in A (\neg x R x \land \forall y \in A \forall z \in A ((x R y \land y R z) \to x R z)))$
32		r19.26	$⊢ \forall x \in A (\neg x R x \land \forall y \in A \forall z \in A ((x R y \land y R z) \to x R z)) \leftrightarrow (\forall x \in A \neg x R x \land \forall x \in A \forall y \in A \forall z \in A ((x R y \land y R z) \to x R z))$
33	31 32	bitrdi	$⊢ A \neq \emptyset \to (\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 x \in A \neg x R x \land \forall x \in A \forall y \in A \forall z \in A ((x R y \land y R z) \to x R z)))$
34		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))$
35		disj	$⊢ R \cap ({I ↾}_{A}) = \emptyset \leftrightarrow \forall w \in R \neg w \in ({I ↾}_{A})$
36		df-ral	$⊢ \forall w \in R \neg w \in ({I ↾}_{A}) \leftrightarrow \forall w (w \in R \to \neg w \in ({I ↾}_{A}))$
37		opex	$⊢ ⟨x, x⟩ \in V$
38		eleq1	$⊢ w = ⟨x, x⟩ \to (w \in R \leftrightarrow ⟨x, x⟩ \in R)$
39		df-br	$⊢ x R x \leftrightarrow ⟨x, x⟩ \in R$
40	38 39	bitr4di	$⊢ w = ⟨x, x⟩ \to (w \in R \leftrightarrow x R x)$
41		eleq1	$⊢ w = ⟨x, x⟩ \to (w \in ({I ↾}_{A}) \leftrightarrow ⟨x, x⟩ \in ({I ↾}_{A}))$
42		opelidres	$⊢ x \in V \to (⟨x, x⟩ \in ({I ↾}_{A}) \leftrightarrow x \in A)$
43	42	elv	$⊢ ⟨x, x⟩ \in ({I ↾}_{A}) \leftrightarrow x \in A$
44	41 43	bitrdi	$⊢ w = ⟨x, x⟩ \to (w \in ({I ↾}_{A}) \leftrightarrow x \in A)$
45	44	notbid	$⊢ w = ⟨x, x⟩ \to (\neg w \in ({I ↾}_{A}) \leftrightarrow \neg x \in A)$
46	40 45	imbi12d	$⊢ w = ⟨x, x⟩ \to ((w \in R \to \neg w \in ({I ↾}_{A})) \leftrightarrow (x R x \to \neg x \in A))$
47	37 46	spcv	$⊢ \forall w (w \in R \to \neg w \in ({I ↾}_{A})) \to (x R x \to \neg x \in A)$
48	47	con2d	$⊢ \forall w (w \in R \to \neg w \in ({I ↾}_{A})) \to (x \in A \to \neg x R x)$
49	48	alrimiv	$⊢ \forall w (w \in R \to \neg w \in ({I ↾}_{A})) \to \forall x (x \in A \to \neg x R x)$
50		relres	$⊢ Rel ({I ↾}_{A})$
51		elrel	$⊢ (Rel ({I ↾}_{A}) \land w \in ({I ↾}_{A})) \to \exists y \exists z w = ⟨y, z⟩$
52	50 51	mpan	$⊢ w \in ({I ↾}_{A}) \to \exists y \exists z w = ⟨y, z⟩$
53	52	ancri	$⊢ w \in ({I ↾}_{A}) \to (\exists y \exists z w = ⟨y, z⟩ \land w \in ({I ↾}_{A}))$
54		eleq1	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
55		breq12	$⊢ (x = y \land x = y) \to (x R x \leftrightarrow y R y)$
56	55	anidms	$⊢ x = y \to (x R x \leftrightarrow y R y)$
57	56	notbid	$⊢ x = y \to (\neg x R x \leftrightarrow \neg y R y)$
58	54 57	imbi12d	$⊢ x = y \to ((x \in A \to \neg x R x) \leftrightarrow (y \in A \to \neg y R y))$
59	58	spvv	$⊢ \forall x (x \in A \to \neg x R x) \to (y \in A \to \neg y R y)$
60		breq2	$⊢ y = z \to (y R y \leftrightarrow y R z)$
61	60	notbid	$⊢ y = z \to (\neg y R y \leftrightarrow \neg y R z)$
62	61	imbi2d	$⊢ y = z \to ((y \in A \to \neg y R y) \leftrightarrow (y \in A \to \neg y R z))$
63	62	biimpcd	$⊢ (y \in A \to \neg y R y) \to (y = z \to (y \in A \to \neg y R z))$
64	63	impcomd	$⊢ (y \in A \to \neg y R y) \to ((y \in A \land y = z) \to \neg y R z)$
65	59 64	syl	$⊢ \forall x (x \in A \to \neg x R x) \to ((y \in A \land y = z) \to \neg y R z)$
66		eleq1	$⊢ w = ⟨y, z⟩ \to (w \in ({I ↾}_{A}) \leftrightarrow ⟨y, z⟩ \in ({I ↾}_{A}))$
67		vex	$⊢ z \in V$
68	67	brresi	$⊢ y ({I ↾}_{A}) z \leftrightarrow (y \in A \land y I z)$
69		df-br	$⊢ y ({I ↾}_{A}) z \leftrightarrow ⟨y, z⟩ \in ({I ↾}_{A})$
70	67	ideq	$⊢ y I z \leftrightarrow y = z$
71	70	anbi2i	$⊢ (y \in A \land y I z) \leftrightarrow (y \in A \land y = z)$
72	68 69 71	3bitr3ri	$⊢ (y \in A \land y = z) \leftrightarrow ⟨y, z⟩ \in ({I ↾}_{A})$
73	66 72	bitr4di	$⊢ w = ⟨y, z⟩ \to (w \in ({I ↾}_{A}) \leftrightarrow (y \in A \land y = z))$
74		eleq1	$⊢ w = ⟨y, z⟩ \to (w \in R \leftrightarrow ⟨y, z⟩ \in R)$
75		df-br	$⊢ y R z \leftrightarrow ⟨y, z⟩ \in R$
76	74 75	bitr4di	$⊢ w = ⟨y, z⟩ \to (w \in R \leftrightarrow y R z)$
77	76	notbid	$⊢ w = ⟨y, z⟩ \to (\neg w \in R \leftrightarrow \neg y R z)$
78	73 77	imbi12d	$⊢ w = ⟨y, z⟩ \to ((w \in ({I ↾}_{A}) \to \neg w \in R) \leftrightarrow ((y \in A \land y = z) \to \neg y R z))$
79	65 78	syl5ibrcom	$⊢ \forall x (x \in A \to \neg x R x) \to (w = ⟨y, z⟩ \to (w \in ({I ↾}_{A}) \to \neg w \in R))$
80	79	exlimdvv	$⊢ \forall x (x \in A \to \neg x R x) \to (\exists y \exists z w = ⟨y, z⟩ \to (w \in ({I ↾}_{A}) \to \neg w \in R))$
81	80	impd	$⊢ \forall x (x \in A \to \neg x R x) \to ((\exists y \exists z w = ⟨y, z⟩ \land w \in ({I ↾}_{A})) \to \neg w \in R)$
82	53 81	syl5	$⊢ \forall x (x \in A \to \neg x R x) \to (w \in ({I ↾}_{A}) \to \neg w \in R)$
83	82	con2d	$⊢ \forall x (x \in A \to \neg x R x) \to (w \in R \to \neg w \in ({I ↾}_{A}))$
84	83	alrimiv	$⊢ \forall x (x \in A \to \neg x R x) \to \forall w (w \in R \to \neg w \in ({I ↾}_{A}))$
85	49 84	impbii	$⊢ \forall w (w \in R \to \neg w \in ({I ↾}_{A})) \leftrightarrow \forall x (x \in A \to \neg x R x)$
86		df-ral	$⊢ \forall x \in A \neg x R x \leftrightarrow \forall x (x \in A \to \neg x R x)$
87	85 86	bitr4i	$⊢ \forall w (w \in R \to \neg w \in ({I ↾}_{A})) \leftrightarrow \forall x \in A \neg x R x$
88	35 36 87	3bitri	$⊢ R \cap ({I ↾}_{A}) = \emptyset \leftrightarrow \forall x \in A \neg x R x$
89		ralcom	$⊢ \forall y \in A \forall z \in A ((x R y \land y R z) \to x R z) \leftrightarrow \forall z \in A \forall y \in A ((x R y \land y R z) \to x R z)$
90		r19.23v	$⊢ \forall y \in A ((x R y \land y R z) \to x R z) \leftrightarrow (\exists y \in A (x R y \land y R z) \to x R z)$
91	90	ralbii	$⊢ \forall z \in A \forall y \in A ((x R y \land y R z) \to x R z) \leftrightarrow \forall z \in A (\exists y \in A (x R y \land y R z) \to x R z)$
92	89 91	bitri	$⊢ \forall y \in A \forall z \in A ((x R y \land y R z) \to x R z) \leftrightarrow \forall z \in A (\exists y \in A (x R y \land y R z) \to x R z)$
93	92	ralbii	$⊢ \forall x \in A \forall y \in A \forall z \in A ((x R y \land y R z) \to x R z) \leftrightarrow \forall x \in A \forall z \in A (\exists y \in A (x R y \land y R z) \to x R z)$
94		brin	$⊢ x (R \cap (A \times A)) y \leftrightarrow (x R y \land x (A \times A) y)$
95		brin	$⊢ y (R \cap (A \times A)) z \leftrightarrow (y R z \land y (A \times A) z)$
96	94 95	anbi12i	$⊢ (x (R \cap (A \times A)) y \land y (R \cap (A \times A)) z) \leftrightarrow ((x R y \land x (A \times A) y) \land (y R z \land y (A \times A) z))$
97		an4	$⊢ ((x R y \land x (A \times A) y) \land (y R z \land y (A \times A) z)) \leftrightarrow ((x R y \land y R z) \land (x (A \times A) y \land y (A \times A) z))$
98		ancom	$⊢ ((x R y \land y R z) \land (x (A \times A) y \land y (A \times A) z)) \leftrightarrow ((x (A \times A) y \land y (A \times A) z) \land (x R y \land y R z))$
99		ancom	$⊢ (x \in A \land y \in A) \leftrightarrow (y \in A \land x \in A)$
100	99	anbi1i	$⊢ ((x \in A \land y \in A) \land (y \in A \land z \in A)) \leftrightarrow ((y \in A \land x \in A) \land (y \in A \land z \in A))$
101		brxp	$⊢ x (A \times A) y \leftrightarrow (x \in A \land y \in A)$
102		brxp	$⊢ y (A \times A) z \leftrightarrow (y \in A \land z \in A)$
103	101 102	anbi12i	$⊢ (x (A \times A) y \land y (A \times A) z) \leftrightarrow ((x \in A \land y \in A) \land (y \in A \land z \in A))$
104		anandi	$⊢ (y \in A \land (x \in A \land z \in A)) \leftrightarrow ((y \in A \land x \in A) \land (y \in A \land z \in A))$
105	100 103 104	3bitr4i	$⊢ (x (A \times A) y \land y (A \times A) z) \leftrightarrow (y \in A \land (x \in A \land z \in A))$
106	105	anbi1i	$⊢ ((x (A \times A) y \land y (A \times A) z) \land (x R y \land y R z)) \leftrightarrow ((y \in A \land (x \in A \land z \in A)) \land (x R y \land y R z))$
107	97 98 106	3bitri	$⊢ ((x R y \land x (A \times A) y) \land (y R z \land y (A \times A) z)) \leftrightarrow ((y \in A \land (x \in A \land z \in A)) \land (x R y \land y R z))$
108		anass	$⊢ ((y \in A \land (x \in A \land z \in A)) \land (x R y \land y R z)) \leftrightarrow (y \in A \land ((x \in A \land z \in A) \land (x R y \land y R z)))$
109	96 107 108	3bitri	$⊢ (x (R \cap (A \times A)) y \land y (R \cap (A \times A)) z) \leftrightarrow (y \in A \land ((x \in A \land z \in A) \land (x R y \land y R z)))$
110	109	exbii	$⊢ \exists y (x (R \cap (A \times A)) y \land y (R \cap (A \times A)) z) \leftrightarrow \exists y (y \in A \land ((x \in A \land z \in A) \land (x R y \land y R z)))$
111		vex	$⊢ x \in V$
112	111 67	brco	$⊢ x ((R \cap (A \times A)) \circ (R \cap (A \times A))) z \leftrightarrow \exists y (x (R \cap (A \times A)) y \land y (R \cap (A \times A)) z)$
113		df-br	$⊢ x ((R \cap (A \times A)) \circ (R \cap (A \times A))) z \leftrightarrow ⟨x, z⟩ \in ((R \cap (A \times A)) \circ (R \cap (A \times A)))$
114	112 113	bitr3i	$⊢ \exists y (x (R \cap (A \times A)) y \land y (R \cap (A \times A)) z) \leftrightarrow ⟨x, z⟩ \in ((R \cap (A \times A)) \circ (R \cap (A \times A)))$
115		df-rex	$⊢ \exists y \in A ((x \in A \land z \in A) \land (x R y \land y R z)) \leftrightarrow \exists y (y \in A \land ((x \in A \land z \in A) \land (x R y \land y R z)))$
116		r19.42v	$⊢ \exists y \in A ((x \in A \land z \in A) \land (x R y \land y R z)) \leftrightarrow ((x \in A \land z \in A) \land \exists y \in A (x R y \land y R z))$
117	115 116	bitr3i	$⊢ \exists y (y \in A \land ((x \in A \land z \in A) \land (x R y \land y R z))) \leftrightarrow ((x \in A \land z \in A) \land \exists y \in A (x R y \land y R z))$
118	110 114 117	3bitr3ri	$⊢ ((x \in A \land z \in A) \land \exists y \in A (x R y \land y R z)) \leftrightarrow ⟨x, z⟩ \in ((R \cap (A \times A)) \circ (R \cap (A \times A)))$
119		df-br	$⊢ x R z \leftrightarrow ⟨x, z⟩ \in R$
120	118 119	imbi12i	$⊢ (((x \in A \land z \in A) \land \exists y \in A (x R y \land y R z)) \to x R z) \leftrightarrow (⟨x, z⟩ \in ((R \cap (A \times A)) \circ (R \cap (A \times A))) \to ⟨x, z⟩ \in R)$
121	120	2albii	$⊢ \forall x \forall z (((x \in A \land z \in A) \land \exists y \in A (x R y \land y R z)) \to x R z) \leftrightarrow \forall x \forall z (⟨x, z⟩ \in ((R \cap (A \times A)) \circ (R \cap (A \times A))) \to ⟨x, z⟩ \in R)$
122		r2al	$⊢ \forall x \in A \forall z \in A (\exists y \in A (x R y \land y R z) \to x R z) \leftrightarrow \forall x \forall z ((x \in A \land z \in A) \to (\exists y \in A (x R y \land y R z) \to x R z))$
123		impexp	$⊢ (((x \in A \land z \in A) \land \exists y \in A (x R y \land y R z)) \to x R z) \leftrightarrow ((x \in A \land z \in A) \to (\exists y \in A (x R y \land y R z) \to x R z))$
124	123	2albii	$⊢ \forall x \forall z (((x \in A \land z \in A) \land \exists y \in A (x R y \land y R z)) \to x R z) \leftrightarrow \forall x \forall z ((x \in A \land z \in A) \to (\exists y \in A (x R y \land y R z) \to x R z))$
125	122 124	bitr4i	$⊢ \forall x \in A \forall z \in A (\exists y \in A (x R y \land y R z) \to x R z) \leftrightarrow \forall x \forall z (((x \in A \land z \in A) \land \exists y \in A (x R y \land y R z)) \to x R z)$
126		relco	$⊢ Rel ((R \cap (A \times A)) \circ (R \cap (A \times A)))$
127		ssrel	$⊢ Rel ((R \cap (A \times A)) \circ (R \cap (A \times A))) \to ((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \leftrightarrow \forall x \forall z (⟨x, z⟩ \in ((R \cap (A \times A)) \circ (R \cap (A \times A))) \to ⟨x, z⟩ \in R))$
128	126 127	ax-mp	$⊢ (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \leftrightarrow \forall x \forall z (⟨x, z⟩ \in ((R \cap (A \times A)) \circ (R \cap (A \times A))) \to ⟨x, z⟩ \in R)$
129	121 125 128	3bitr4i	$⊢ \forall x \in A \forall z \in A (\exists y \in A (x R y \land y R z) \to x R z) \leftrightarrow (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R$
130	93 129	bitr2i	$⊢ (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \leftrightarrow \forall x \in A \forall y \in A \forall z \in A ((x R y \land y R z) \to x R z)$
131	88 130	anbi12i	$⊢ (R \cap ({I ↾}_{A}) = \emptyset \land (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R) \leftrightarrow (\forall x \in A \neg x R x \land \forall x \in A \forall y \in A \forall z \in A ((x R y \land y R z) \to x R z))$
132	33 34 131	3bitr4g	$⊢ A \neq \emptyset \to (R Po A \leftrightarrow (R \cap ({I ↾}_{A}) = \emptyset \land (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R))$
133	26 132	pm2.61ine	$⊢ R Po A \leftrightarrow (R \cap ({I ↾}_{A}) = \emptyset \land (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R)$

Metamath Proof Explorer

Theorem dfpo2

Proof