Metamath Proof Explorer


Theorem slttrine

Description: Trichotomy law for surreals. (Contributed by Scott Fenton, 23-Nov-2021)

Ref Expression
Assertion slttrine ( ( 𝐴 No 𝐵 No ) → ( 𝐴𝐵 ↔ ( 𝐴 <s 𝐵𝐵 <s 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 sltso <s Or No
2 sotrine ( ( <s Or No ∧ ( 𝐴 No 𝐵 No ) ) → ( 𝐴𝐵 ↔ ( 𝐴 <s 𝐵𝐵 <s 𝐴 ) ) )
3 1 2 mpan ( ( 𝐴 No 𝐵 No ) → ( 𝐴𝐵 ↔ ( 𝐴 <s 𝐵𝐵 <s 𝐴 ) ) )