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

Proof

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