This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 ↔ ¬ ( 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) )