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 ≤ s B ∧ B ≤ s A

Proof

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