Metamath Proof Explorer

Theorem ltnles

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

Ref Expression
Assertion ltnles ⊢ A ∈ No ∧ B ∈ No → A < s B ↔ ¬ B ≤ s A

Proof

Step Hyp Ref Expression
1 lenlts ⊢ B ∈ No ∧ A ∈ No → B ≤ s A ↔ ¬ A < s B
2 1 ancoms ⊢ A ∈ No ∧ B ∈ No → B ≤ s A ↔ ¬ A < s B
3 2 con2bid ⊢ A ∈ No ∧ B ∈ No → A < s B ↔ ¬ B ≤ s A