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 = (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))$
	swoso.4	$⊢ φ \to Y \subseteq X$
	swoso.5	$⊢ (φ \land (x \in Y \land y \in Y \land x R y)) \to x = y$
Assertion	swoso	$⊢ φ \to \underset{˙}{<} Or Y$

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

Metamath Proof Explorer

Theorem swoso

Proof