Theorem swoso

Description: If the incomparability relation is equivalent to equality in a subset, then the partial order strictly orders the subset. (Contributed by Mario Carneiro, 30-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)$$
	swoso.4	$$⊢\phi \to Y\subseteq X$$
	swoso.5	$$⊢\left(\phi \wedge \left(x\in Y\wedge y\in Y\wedge xRy\right)\right)\to x=y$$
Assertion	swoso	$$⊢\phi \to \underset{\dot{}}{<}\mathrm{Or}Y$$

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		swoso.4	$$⊢\phi \to Y\subseteq X$$
5		swoso.5	$$⊢\left(\phi \wedge \left(x\in Y\wedge y\in Y\wedge xRy\right)\right)\to x=y$$
6	2 3	swopo	$$⊢\phi \to \underset{\dot{}}{<}\mathrm{Po}X$$
7		poss	$$⊢Y\subseteq X\to \left(\underset{\dot{}}{<}\mathrm{Po}X\to \underset{\dot{}}{<}\mathrm{Po}Y\right)$$
8	4 6 7	sylc	$$⊢\phi \to \underset{\dot{}}{<}\mathrm{Po}Y$$
9	4	sselda	$$⊢\left(\phi \wedge x\in Y\right)\to x\in X$$
10	4	sselda	$$⊢\left(\phi \wedge y\in Y\right)\to y\in X$$
11	9 10	anim12dan	$$⊢\left(\phi \wedge \left(x\in Y\wedge y\in Y\right)\right)\to \left(x\in X\wedge y\in X\right)$$
12	1	brdifun	$$⊢\left(x\in X\wedge y\in X\right)\to \left(xRy\leftrightarrow \neg \left(x\underset{\dot{}}{<}y\vee y\underset{\dot{}}{<}x\right)\right)$$
13	11 12	syl	$$⊢\left(\phi \wedge \left(x\in Y\wedge y\in Y\right)\right)\to \left(xRy\leftrightarrow \neg \left(x\underset{\dot{}}{<}y\vee y\underset{\dot{}}{<}x\right)\right)$$
14		df-3an	$$⊢\left(x\in Y\wedge y\in Y\wedge xRy\right)\leftrightarrow \left(\left(x\in Y\wedge y\in Y\right)\wedge xRy\right)$$
15	14 5	sylan2br	$$⊢\left(\phi \wedge \left(\left(x\in Y\wedge y\in Y\right)\wedge xRy\right)\right)\to x=y$$
16	15	expr	$$⊢\left(\phi \wedge \left(x\in Y\wedge y\in Y\right)\right)\to \left(xRy\to x=y\right)$$
17	13 16	sylbird	$$⊢\left(\phi \wedge \left(x\in Y\wedge y\in Y\right)\right)\to \left(\neg \left(x\underset{\dot{}}{<}y\vee y\underset{\dot{}}{<}x\right)\to x=y\right)$$
18	17	orrd	$$⊢\left(\phi \wedge \left(x\in Y\wedge y\in Y\right)\right)\to \left(\left(x\underset{\dot{}}{<}y\vee y\underset{\dot{}}{<}x\right)\vee x=y\right)$$
19		3orcomb	$$⊢\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\leftrightarrow \left(x\underset{\dot{}}{<}y\vee y\underset{\dot{}}{<}x\vee x=y\right)$$
20		df-3or	$$⊢\left(x\underset{\dot{}}{<}y\vee y\underset{\dot{}}{<}x\vee x=y\right)\leftrightarrow \left(\left(x\underset{\dot{}}{<}y\vee y\underset{\dot{}}{<}x\right)\vee x=y\right)$$
21	19 20	bitri	$$⊢\left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)\leftrightarrow \left(\left(x\underset{\dot{}}{<}y\vee y\underset{\dot{}}{<}x\right)\vee x=y\right)$$
22	18 21	sylibr	$$⊢\left(\phi \wedge \left(x\in Y\wedge y\in Y\right)\right)\to \left(x\underset{\dot{}}{<}y\vee x=y\vee y\underset{\dot{}}{<}x\right)$$
23	8 22	issod	$$⊢\phi \to \underset{\dot{}}{<}\mathrm{Or}Y$$