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

Metamath Proof Explorer

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