Metamath Proof Explorer

Theorem lesloe

Description: Surreal less-than or equal in terms of less-than. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion lesloe ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ↔ A < s B ∨ A = B

Proof

Step Hyp Ref Expression
1 lenlts ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ↔ ¬ B < s A
2 orcom ⊢ A < s B ∨ A = B ↔ A = B ∨ A < s B
3 eqcom ⊢ A = B ↔ B = A
4 3 orbi1i ⊢ A = B ∨ A < s B ↔ B = A ∨ A < s B
5 2 4 bitri ⊢ A < s B ∨ A = B ↔ B = A ∨ A < s B
6 ltsso ⊢ < s Or No
7 sotric ⊢ < s Or No ∧ B ∈ No ∧ A ∈ No → B < s A ↔ ¬ B = A ∨ A < s B
8 6 7 mpan ⊢ B ∈ No ∧ A ∈ No → B < s A ↔ ¬ B = A ∨ A < s B
9 8 ancoms ⊢ A ∈ No ∧ B ∈ No → B < s A ↔ ¬ B = A ∨ A < s B
10 9 con2bid ⊢ A ∈ No ∧ B ∈ No → B = A ∨ A < s B ↔ ¬ B < s A
11 5 10 bitrid ⊢ A ∈ No ∧ B ∈ No → A < s B ∨ A = B ↔ ¬ B < s A
12 1 11 bitr4d ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ↔ A < s B ∨ A = B