Metamath Proof Explorer

Theorem ltlesnd

Description: Surreal less-than in terms of less-than or equal. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Hypotheses ltlesn.1 ⊢ φ → A ∈ No
ltlesn.2 ⊢ φ → B ∈ No
Assertion ltlesnd ⊢ φ → A < s B ↔ A ≤ s B ∧ B ≠ A

Proof

Step Hyp Ref Expression
1 ltlesn.1 ⊢ φ → A ∈ No
2 ltlesn.2 ⊢ φ → B ∈ No
3 1 adantr ⊢ φ ∧ A < s B → A ∈ No
4 2 adantr ⊢ φ ∧ A < s B → B ∈ No
5 simpr ⊢ φ ∧ A < s B → A < s B
6 3 4 5 ltlesd ⊢ φ ∧ A < s B → A ≤ s B
7 6 ex ⊢ φ → A < s B → A ≤ s B
8 ltsne ⊢ A ∈ No ∧ A < s B → B ≠ A
9 1 8 sylan ⊢ φ ∧ A < s B → B ≠ A
10 9 ex ⊢ φ → A < s B → B ≠ A
11 7 10 jcad ⊢ φ → A < s B → A ≤ s B ∧ B ≠ A
12 lesloe ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ↔ A < s B ∨ A = B
13 1 2 12 syl2anc ⊢ φ → A ≤ s B ↔ A < s B ∨ A = B
14 eqneqall ⊢ B = A → B ≠ A → A < s B
15 14 eqcoms ⊢ A = B → B ≠ A → A < s B
16 15 jao1i ⊢ A < s B ∨ A = B → B ≠ A → A < s B
17 13 16 biimtrdi ⊢ φ → A ≤ s B → B ≠ A → A < s B
18 17 impd ⊢ φ → A ≤ s B ∧ B ≠ A → A < s B
19 11 18 impbid ⊢ φ → A < s B ↔ A ≤ s B ∧ B ≠ A