Theorem sotrieq

Description: Trichotomy law for strict order relation. (Contributed by NM, 9-Apr-1996) (Proof shortened by Andrew Salmon, 25-Jul-2011)

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

Proof

Step	Hyp	Ref	Expression
1		sonr	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 𝑅 𝐵 )
2	1	adantrr	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ¬ 𝐵 𝑅 𝐵 )
3		pm1.2	⊢ ( ( 𝐵 𝑅 𝐵 ∨ 𝐵 𝑅 𝐵 ) → 𝐵 𝑅 𝐵 )
4	2 3	nsyl	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐵 ∨ 𝐵 𝑅 𝐵 ) )
5		breq2	⊢ ( 𝐵 = 𝐶 → ( 𝐵 𝑅 𝐵 ↔ 𝐵 𝑅 𝐶 ) )
6		breq1	⊢ ( 𝐵 = 𝐶 → ( 𝐵 𝑅 𝐵 ↔ 𝐶 𝑅 𝐵 ) )
7	5 6	orbi12d	⊢ ( 𝐵 = 𝐶 → ( ( 𝐵 𝑅 𝐵 ∨ 𝐵 𝑅 𝐵 ) ↔ ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
8	7	notbid	⊢ ( 𝐵 = 𝐶 → ( ¬ ( 𝐵 𝑅 𝐵 ∨ 𝐵 𝑅 𝐵 ) ↔ ¬ ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
9	4 8	syl5ibcom	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 = 𝐶 → ¬ ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
10	9	con2d	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) → ¬ 𝐵 = 𝐶 ) )
11		solin	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) )
12		3orass	⊢ ( ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ↔ ( 𝐵 𝑅 𝐶 ∨ ( 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
13	11 12	sylib	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 ∨ ( 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
14		or12	⊢ ( ( 𝐵 𝑅 𝐶 ∨ ( 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) ↔ ( 𝐵 = 𝐶 ∨ ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
15	13 14	sylib	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 = 𝐶 ∨ ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
16	15	ord	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ¬ 𝐵 = 𝐶 → ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
17	10 16	impbid	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) ↔ ¬ 𝐵 = 𝐶 ) )
18	17	con2bid	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )