swoer

Description: Incomparability under a strict weak partial order is an equivalence relation. (Contributed by Mario Carneiro, 9-Jul-2014) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypotheses	swoer.1	$⊢ R = (X \times X) ∖ (\underset{˙}{<} \cup {\underset{˙}{<}}^{-1})$
	swoer.2	$⊢ (φ \land (y \in X \land z \in X)) \to (y \underset{˙}{<} z \to \neg z \underset{˙}{<} y)$
	swoer.3	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x \underset{˙}{<} y \to (x \underset{˙}{<} z \lor z \underset{˙}{<} y))$
Assertion	swoer	$⊢ φ \to R Er X$

Proof

Step	Hyp	Ref	Expression
1		swoer.1	$⊢ R = (X \times X) ∖ (\underset{˙}{<} \cup {\underset{˙}{<}}^{-1})$
2		swoer.2	$⊢ (φ \land (y \in X \land z \in X)) \to (y \underset{˙}{<} z \to \neg z \underset{˙}{<} y)$
3		swoer.3	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x \underset{˙}{<} y \to (x \underset{˙}{<} z \lor z \underset{˙}{<} y))$
4		difss	$⊢ (X \times X) ∖ (\underset{˙}{<} \cup {\underset{˙}{<}}^{-1}) \subseteq X \times X$
5	1 4	eqsstri	$⊢ R \subseteq X \times X$
6		relxp	$⊢ Rel (X \times X)$
7		relss	$⊢ R \subseteq X \times X \to (Rel (X \times X) \to Rel R)$
8	5 6 7	mp2	$⊢ Rel R$
9	8	a1i	$⊢ φ \to Rel R$
10		simpr	$⊢ (φ \land u R v) \to u R v$
11		orcom	$⊢ (u \underset{˙}{<} v \lor v \underset{˙}{<} u) \leftrightarrow (v \underset{˙}{<} u \lor u \underset{˙}{<} v)$
12	11	a1i	$⊢ (φ \land u R v) \to ((u \underset{˙}{<} v \lor v \underset{˙}{<} u) \leftrightarrow (v \underset{˙}{<} u \lor u \underset{˙}{<} v))$
13	12	notbid	$⊢ (φ \land u R v) \to (\neg (u \underset{˙}{<} v \lor v \underset{˙}{<} u) \leftrightarrow \neg (v \underset{˙}{<} u \lor u \underset{˙}{<} v))$
14	5	ssbri	$⊢ u R v \to u (X \times X) v$
15	14	adantl	$⊢ (φ \land u R v) \to u (X \times X) v$
16		brxp	$⊢ u (X \times X) v \leftrightarrow (u \in X \land v \in X)$
17	15 16	sylib	$⊢ (φ \land u R v) \to (u \in X \land v \in X)$
18	1	brdifun	$⊢ (u \in X \land v \in X) \to (u R v \leftrightarrow \neg (u \underset{˙}{<} v \lor v \underset{˙}{<} u))$
19	17 18	syl	$⊢ (φ \land u R v) \to (u R v \leftrightarrow \neg (u \underset{˙}{<} v \lor v \underset{˙}{<} u))$
20	17	simprd	$⊢ (φ \land u R v) \to v \in X$
21	17	simpld	$⊢ (φ \land u R v) \to u \in X$
22	1	brdifun	$⊢ (v \in X \land u \in X) \to (v R u \leftrightarrow \neg (v \underset{˙}{<} u \lor u \underset{˙}{<} v))$
23	20 21 22	syl2anc	$⊢ (φ \land u R v) \to (v R u \leftrightarrow \neg (v \underset{˙}{<} u \lor u \underset{˙}{<} v))$
24	13 19 23	3bitr4d	$⊢ (φ \land u R v) \to (u R v \leftrightarrow v R u)$
25	10 24	mpbid	$⊢ (φ \land u R v) \to v R u$
26		simprl	$⊢ (φ \land (u R v \land v R w)) \to u R v$
27	14	ad2antrl	$⊢ (φ \land (u R v \land v R w)) \to u (X \times X) v$
28	16	simplbi	$⊢ u (X \times X) v \to u \in X$
29	27 28	syl	$⊢ (φ \land (u R v \land v R w)) \to u \in X$
30	16	simprbi	$⊢ u (X \times X) v \to v \in X$
31	27 30	syl	$⊢ (φ \land (u R v \land v R w)) \to v \in X$
32	29 31 18	syl2anc	$⊢ (φ \land (u R v \land v R w)) \to (u R v \leftrightarrow \neg (u \underset{˙}{<} v \lor v \underset{˙}{<} u))$
33	26 32	mpbid	$⊢ (φ \land (u R v \land v R w)) \to \neg (u \underset{˙}{<} v \lor v \underset{˙}{<} u)$
34		simprr	$⊢ (φ \land (u R v \land v R w)) \to v R w$
35	5	brel	$⊢ v R w \to (v \in X \land w \in X)$
36	35	simprd	$⊢ v R w \to w \in X$
37	34 36	syl	$⊢ (φ \land (u R v \land v R w)) \to w \in X$
38	1	brdifun	$⊢ (v \in X \land w \in X) \to (v R w \leftrightarrow \neg (v \underset{˙}{<} w \lor w \underset{˙}{<} v))$
39	31 37 38	syl2anc	$⊢ (φ \land (u R v \land v R w)) \to (v R w \leftrightarrow \neg (v \underset{˙}{<} w \lor w \underset{˙}{<} v))$
40	34 39	mpbid	$⊢ (φ \land (u R v \land v R w)) \to \neg (v \underset{˙}{<} w \lor w \underset{˙}{<} v)$
41		simpl	$⊢ (φ \land (u R v \land v R w)) \to φ$
42	3	swopolem	$⊢ (φ \land (u \in X \land w \in X \land v \in X)) \to (u \underset{˙}{<} w \to (u \underset{˙}{<} v \lor v \underset{˙}{<} w))$
43	41 29 37 31 42	syl13anc	$⊢ (φ \land (u R v \land v R w)) \to (u \underset{˙}{<} w \to (u \underset{˙}{<} v \lor v \underset{˙}{<} w))$
44	3	swopolem	$⊢ (φ \land (w \in X \land u \in X \land v \in X)) \to (w \underset{˙}{<} u \to (w \underset{˙}{<} v \lor v \underset{˙}{<} u))$
45	41 37 29 31 44	syl13anc	$⊢ (φ \land (u R v \land v R w)) \to (w \underset{˙}{<} u \to (w \underset{˙}{<} v \lor v \underset{˙}{<} u))$
46		orcom	$⊢ (v \underset{˙}{<} u \lor w \underset{˙}{<} v) \leftrightarrow (w \underset{˙}{<} v \lor v \underset{˙}{<} u)$
47	45 46	imbitrrdi	$⊢ (φ \land (u R v \land v R w)) \to (w \underset{˙}{<} u \to (v \underset{˙}{<} u \lor w \underset{˙}{<} v))$
48	43 47	orim12d	$⊢ (φ \land (u R v \land v R w)) \to ((u \underset{˙}{<} w \lor w \underset{˙}{<} u) \to ((u \underset{˙}{<} v \lor v \underset{˙}{<} w) \lor (v \underset{˙}{<} u \lor w \underset{˙}{<} v)))$
49		or4	$⊢ ((u \underset{˙}{<} v \lor v \underset{˙}{<} w) \lor (v \underset{˙}{<} u \lor w \underset{˙}{<} v)) \leftrightarrow ((u \underset{˙}{<} v \lor v \underset{˙}{<} u) \lor (v \underset{˙}{<} w \lor w \underset{˙}{<} v))$
50	48 49	imbitrdi	$⊢ (φ \land (u R v \land v R w)) \to ((u \underset{˙}{<} w \lor w \underset{˙}{<} u) \to ((u \underset{˙}{<} v \lor v \underset{˙}{<} u) \lor (v \underset{˙}{<} w \lor w \underset{˙}{<} v)))$
51	33 40 50	mtord	$⊢ (φ \land (u R v \land v R w)) \to \neg (u \underset{˙}{<} w \lor w \underset{˙}{<} u)$
52	1	brdifun	$⊢ (u \in X \land w \in X) \to (u R w \leftrightarrow \neg (u \underset{˙}{<} w \lor w \underset{˙}{<} u))$
53	29 37 52	syl2anc	$⊢ (φ \land (u R v \land v R w)) \to (u R w \leftrightarrow \neg (u \underset{˙}{<} w \lor w \underset{˙}{<} u))$
54	51 53	mpbird	$⊢ (φ \land (u R v \land v R w)) \to u R w$
55	2 3	swopo	$⊢ φ \to \underset{˙}{<} Po X$
56		poirr	$⊢ (\underset{˙}{<} Po X \land u \in X) \to \neg u \underset{˙}{<} u$
57	55 56	sylan	$⊢ (φ \land u \in X) \to \neg u \underset{˙}{<} u$
58		pm1.2	$⊢ (u \underset{˙}{<} u \lor u \underset{˙}{<} u) \to u \underset{˙}{<} u$
59	57 58	nsyl	$⊢ (φ \land u \in X) \to \neg (u \underset{˙}{<} u \lor u \underset{˙}{<} u)$
60		simpr	$⊢ (φ \land u \in X) \to u \in X$
61	1	brdifun	$⊢ (u \in X \land u \in X) \to (u R u \leftrightarrow \neg (u \underset{˙}{<} u \lor u \underset{˙}{<} u))$
62	60 60 61	syl2anc	$⊢ (φ \land u \in X) \to (u R u \leftrightarrow \neg (u \underset{˙}{<} u \lor u \underset{˙}{<} u))$
63	59 62	mpbird	$⊢ (φ \land u \in X) \to u R u$
64	5	ssbri	$⊢ u R u \to u (X \times X) u$
65		brxp	$⊢ u (X \times X) u \leftrightarrow (u \in X \land u \in X)$
66	65	simplbi	$⊢ u (X \times X) u \to u \in X$
67	64 66	syl	$⊢ u R u \to u \in X$
68	67	adantl	$⊢ (φ \land u R u) \to u \in X$
69	63 68	impbida	$⊢ φ \to (u \in X \leftrightarrow u R u)$
70	9 25 54 69	iserd	$⊢ φ \to R Er X$

Metamath Proof Explorer

Theorem swoer

Proof