Theorem sotrieq2

Description: Trichotomy law for strict order relation. (Contributed by NM, 5-May-1999)

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

Proof

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