sotric

Description: A strict order relation satisfies strict trichotomy. (Contributed by NM, 19-Feb-1996)

		Ref	Expression
	Assertion	sotric	$⊢ (R Or A \land (B \in A \land C \in A)) \to (B R C \leftrightarrow \neg (B = C \lor C R B))$

Step	Hyp	Ref	Expression
1		sonr	$⊢ (R Or A \land B \in A) \to \neg B R B$
2		breq2	$⊢ B = C \to (B R B \leftrightarrow B R C)$
3	2	notbid	$⊢ B = C \to (\neg B R B \leftrightarrow \neg B R C)$
4	1 3	syl5ibcom	$⊢ (R Or A \land B \in A) \to (B = C \to \neg B R C)$
5	4	adantrr	$⊢ (R Or A \land (B \in A \land C \in A)) \to (B = C \to \neg B R C)$
6		so2nr	$⊢ (R Or A \land (B \in A \land C \in A)) \to \neg (B R C \land C R B)$
7		imnan	$⊢ (B R C \to \neg C R B) \leftrightarrow \neg (B R C \land C R B)$
8	6 7	sylibr	$⊢ (R Or A \land (B \in A \land C \in A)) \to (B R C \to \neg C R B)$
9	8	con2d	$⊢ (R Or A \land (B \in A \land C \in A)) \to (C R B \to \neg B R C)$
10	5 9	jaod	$⊢ (R Or A \land (B \in A \land C \in A)) \to ((B = C \lor C R B) \to \neg B R C)$
11		solin	$⊢ (R Or A \land (B \in A \land C \in A)) \to (B R C \lor B = C \lor C R B)$
12		3orass	$⊢ (B R C \lor B = C \lor C R B) \leftrightarrow (B R C \lor (B = C \lor C R B))$
13	11 12	sylib	$⊢ (R Or A \land (B \in A \land C \in A)) \to (B R C \lor (B = C \lor C R B))$
14	13	ord	$⊢ (R Or A \land (B \in A \land C \in A)) \to (\neg B R C \to (B = C \lor C R B))$
15	10 14	impbid	$⊢ (R Or A \land (B \in A \land C \in A)) \to ((B = C \lor C R B) \leftrightarrow \neg B R C)$
16	15	con2bid	$⊢ (R Or A \land (B \in A \land C \in A)) \to (B R C \leftrightarrow \neg (B = C \lor C R B))$

Metamath Proof Explorer