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 ⊢ROrA∧B∈A∧C∈A→B=C↔¬BRC∨CRB

Proof

Step Hyp Ref Expression
1 sonr ⊢ROrA∧B∈A→¬BRB
2 1 adantrr ⊢ROrA∧B∈A∧C∈A→¬BRB
3 pm1.2 ⊢BRB∨BRB→BRB
4 2 3 nsyl ⊢ROrA∧B∈A∧C∈A→¬BRB∨BRB
5 breq2 ⊢B=C→BRB↔BRC
6 breq1 ⊢B=C→BRB↔CRB
7 5 6 orbi12d ⊢B=C→BRB∨BRB↔BRC∨CRB
8 7 notbid ⊢B=C→¬BRB∨BRB↔¬BRC∨CRB
9 4 8 syl5ibcom ⊢ROrA∧B∈A∧C∈A→B=C→¬BRC∨CRB
10 9 con2d ⊢ROrA∧B∈A∧C∈A→BRC∨CRB→¬B=C
11 solin ⊢ROrA∧B∈A∧C∈A→BRC∨B=C∨CRB
12 3orass ⊢BRC∨B=C∨CRB↔BRC∨B=C∨CRB
13 11 12 sylib ⊢ROrA∧B∈A∧C∈A→BRC∨B=C∨CRB
14 or12 ⊢BRC∨B=C∨CRB↔B=C∨BRC∨CRB
15 13 14 sylib ⊢ROrA∧B∈A∧C∈A→B=C∨BRC∨CRB
16 15 ord ⊢ROrA∧B∈A∧C∈A→¬B=C→BRC∨CRB
17 10 16 impbid ⊢ROrA∧B∈A∧C∈A→BRC∨CRB↔¬B=C
18 17 con2bid ⊢ROrA∧B∈A∧C∈A→B=C↔¬BRC∨CRB