Theorem sotrine

Description: Trichotomy law for strict orderings. (Contributed by Scott Fenton, 8-Dec-2021)

	Ref	Expression
Assertion	sotrine	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 ≠ 𝐶 ↔ ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sotrieq	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )
2	1	bicomd	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ¬ ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) ↔ 𝐵 = 𝐶 ) )
3	2	necon1abid	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 ≠ 𝐶 ↔ ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )