Metamath Proof Explorer

Theorem slenlt

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

Ref Expression
Assertion slenlt ⊢A∈No∧B∈No→A≤sB↔¬B<sA

Proof

Step Hyp Ref Expression
1 df-sle ⊢≤s=No×No∖<s-1
2 1 breqi ⊢A≤sB↔ANo×No∖<s-1B
3 brdif ⊢ANo×No∖<s-1B↔ANo×NoB∧¬A<s-1B
4 brxp ⊢ANo×NoB↔A∈No∧B∈No
5 4 anbi1i ⊢ANo×NoB∧¬A<s-1B↔A∈No∧B∈No∧¬A<s-1B
6 2 3 5 3bitri ⊢A≤sB↔A∈No∧B∈No∧¬A<s-1B
7 ibar ⊢A∈No∧B∈No→¬A<s-1B↔A∈No∧B∈No∧¬A<s-1B
8 brcnvg ⊢A∈No∧B∈No→A<s-1B↔B<sA
9 8 notbid ⊢A∈No∧B∈No→¬A<s-1B↔¬B<sA
10 7 9 bitr3d ⊢A∈No∧B∈No→A∈No∧B∈No∧¬A<s-1B↔¬B<sA
11 6 10 bitrid ⊢A∈No∧B∈No→A≤sB↔¬B<sA