Metamath Proof Explorer
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 𝐴 ) ) ) |