Theorem swoord1

Description: The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014)

	Ref	Expression
Hypotheses	swoer.1	$$⊢R=\left(X\times X\right)\setminus \left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)$$
	swoer.2	$$⊢\left(\phi \wedge \left(y\in X\wedge z\in X\right)\right)\to \left(y\underset{\dot{}}{<}z\to \neg z\underset{\dot{}}{<}y\right)$$
	swoer.3	$$⊢\left(\phi \wedge \left(x\in X\wedge y\in X\wedge z\in X\right)\right)\to \left(x\underset{\dot{}}{<}y\to \left(x\underset{\dot{}}{<}z\vee z\underset{\dot{}}{<}y\right)\right)$$
	swoord.4	$$⊢\phi \to B\in X$$
	swoord.5	$$⊢\phi \to C\in X$$
	swoord.6	$$⊢\phi \to ARB$$
Assertion	swoord1	$$⊢\phi \to \left(A\underset{\dot{}}{<}C\leftrightarrow B\underset{\dot{}}{<}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		swoer.1	$$⊢R=\left(X\times X\right)\setminus \left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)$$
2		swoer.2	$$⊢\left(\phi \wedge \left(y\in X\wedge z\in X\right)\right)\to \left(y\underset{\dot{}}{<}z\to \neg z\underset{\dot{}}{<}y\right)$$
3		swoer.3	$$⊢\left(\phi \wedge \left(x\in X\wedge y\in X\wedge z\in X\right)\right)\to \left(x\underset{\dot{}}{<}y\to \left(x\underset{\dot{}}{<}z\vee z\underset{\dot{}}{<}y\right)\right)$$
4		swoord.4	$$⊢\phi \to B\in X$$
5		swoord.5	$$⊢\phi \to C\in X$$
6		swoord.6	$$⊢\phi \to ARB$$
7		id	$$⊢\phi \to \phi$$
8		difss	$$⊢\left(X\times X\right)\setminus \left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)\subseteq X\times X$$
9	1 8	eqsstri	$$⊢R\subseteq X\times X$$
10	9	ssbri	$$⊢ARB\to A\left(X\times X\right)B$$
11		df-br	$$⊢A\left(X\times X\right)B\leftrightarrow ⟨A,B⟩\in \left(X\times X\right)$$
12		opelxp1	$$⊢⟨A,B⟩\in \left(X\times X\right)\to A\in X$$
13	11 12	sylbi	$$⊢A\left(X\times X\right)B\to A\in X$$
14	6 10 13	3syl	$$⊢\phi \to A\in X$$
15	3	swopolem	$$⊢\left(\phi \wedge \left(A\in X\wedge C\in X\wedge B\in X\right)\right)\to \left(A\underset{\dot{}}{<}C\to \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}C\right)\right)$$
16	7 14 5 4 15	syl13anc	$$⊢\phi \to \left(A\underset{\dot{}}{<}C\to \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}C\right)\right)$$
17	1	brdifun	$$⊢\left(A\in X\wedge B\in X\right)\to \left(ARB\leftrightarrow \neg \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}A\right)\right)$$
18	14 4 17	syl2anc	$$⊢\phi \to \left(ARB\leftrightarrow \neg \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}A\right)\right)$$
19	6 18	mpbid	$$⊢\phi \to \neg \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}A\right)$$
20		orc	$$⊢A\underset{\dot{}}{<}B\to \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}A\right)$$
21	19 20	nsyl	$$⊢\phi \to \neg A\underset{\dot{}}{<}B$$
22		biorf	$$⊢\neg A\underset{\dot{}}{<}B\to \left(B\underset{\dot{}}{<}C\leftrightarrow \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}C\right)\right)$$
23	21 22	syl	$$⊢\phi \to \left(B\underset{\dot{}}{<}C\leftrightarrow \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}C\right)\right)$$
24	16 23	sylibrd	$$⊢\phi \to \left(A\underset{\dot{}}{<}C\to B\underset{\dot{}}{<}C\right)$$
25	3	swopolem	$$⊢\left(\phi \wedge \left(B\in X\wedge C\in X\wedge A\in X\right)\right)\to \left(B\underset{\dot{}}{<}C\to \left(B\underset{\dot{}}{<}A\vee A\underset{\dot{}}{<}C\right)\right)$$
26	7 4 5 14 25	syl13anc	$$⊢\phi \to \left(B\underset{\dot{}}{<}C\to \left(B\underset{\dot{}}{<}A\vee A\underset{\dot{}}{<}C\right)\right)$$
27		olc	$$⊢B\underset{\dot{}}{<}A\to \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}A\right)$$
28	19 27	nsyl	$$⊢\phi \to \neg B\underset{\dot{}}{<}A$$
29		biorf	$$⊢\neg B\underset{\dot{}}{<}A\to \left(A\underset{\dot{}}{<}C\leftrightarrow \left(B\underset{\dot{}}{<}A\vee A\underset{\dot{}}{<}C\right)\right)$$
30	28 29	syl	$$⊢\phi \to \left(A\underset{\dot{}}{<}C\leftrightarrow \left(B\underset{\dot{}}{<}A\vee A\underset{\dot{}}{<}C\right)\right)$$
31	26 30	sylibrd	$$⊢\phi \to \left(B\underset{\dot{}}{<}C\to A\underset{\dot{}}{<}C\right)$$
32	24 31	impbid	$$⊢\phi \to \left(A\underset{\dot{}}{<}C\leftrightarrow B\underset{\dot{}}{<}C\right)$$