Metamath Proof Explorer

Theorem sletri3

Description: Trichotomy law for surreal less-than or equal. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion sletri3 ⊢A∈No∧B∈No→A=B↔A≤sB∧B≤sA

Proof

Step Hyp Ref Expression
1 slttrieq2 ⊢A∈No∧B∈No→A=B↔¬A<sB∧¬B<sA
2 slenlt ⊢A∈No∧B∈No→A≤sB↔¬B<sA
3 slenlt ⊢B∈No∧A∈No→B≤sA↔¬A<sB
4 3 ancoms ⊢A∈No∧B∈No→B≤sA↔¬A<sB
5 2 4 anbi12d ⊢A∈No∧B∈No→A≤sB∧B≤sA↔¬B<sA∧¬A<sB
6 ancom ⊢¬B<sA∧¬A<sB↔¬A<sB∧¬B<sA
7 5 6 bitrdi ⊢A∈No∧B∈No→A≤sB∧B≤sA↔¬A<sB∧¬B<sA
8 1 7 bitr4d ⊢A∈No∧B∈No→A=B↔A≤sB∧B≤sA