Theorem sotric

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

	Ref	Expression
Assertion	sotric	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 ↔ ¬ ( 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sonr	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 𝑅 𝐵 )
2		breq2	⊢ ( 𝐵 = 𝐶 → ( 𝐵 𝑅 𝐵 ↔ 𝐵 𝑅 𝐶 ) )
3	2	notbid	⊢ ( 𝐵 = 𝐶 → ( ¬ 𝐵 𝑅 𝐵 ↔ ¬ 𝐵 𝑅 𝐶 ) )
4	1 3	syl5ibcom	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐵 = 𝐶 → ¬ 𝐵 𝑅 𝐶 ) )
5	4	adantrr	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 = 𝐶 → ¬ 𝐵 𝑅 𝐶 ) )
6		so2nr	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) )
7		imnan	⊢ ( ( 𝐵 𝑅 𝐶 → ¬ 𝐶 𝑅 𝐵 ) ↔ ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) )
8	6 7	sylibr	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 → ¬ 𝐶 𝑅 𝐵 ) )
9	8	con2d	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐶 𝑅 𝐵 → ¬ 𝐵 𝑅 𝐶 ) )
10	5 9	jaod	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ( 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) → ¬ 𝐵 𝑅 𝐶 ) )
11		solin	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) )
12		3orass	⊢ ( ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ↔ ( 𝐵 𝑅 𝐶 ∨ ( 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
13	11 12	sylib	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 ∨ ( 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
14	13	ord	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ¬ 𝐵 𝑅 𝐶 → ( 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
15	10 14	impbid	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ( 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ↔ ¬ 𝐵 𝑅 𝐶 ) )
16	15	con2bid	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 ↔ ¬ ( 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )