Metamath Proof Explorer


Theorem sltlend

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

Ref Expression
Hypotheses sltlen.1 ( 𝜑𝐴 No )
sltlen.2 ( 𝜑𝐵 No )
Assertion sltlend ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( 𝐴 ≤s 𝐵𝐵𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 sltlen.1 ( 𝜑𝐴 No )
2 sltlen.2 ( 𝜑𝐵 No )
3 1 adantr ( ( 𝜑𝐴 <s 𝐵 ) → 𝐴 No )
4 2 adantr ( ( 𝜑𝐴 <s 𝐵 ) → 𝐵 No )
5 simpr ( ( 𝜑𝐴 <s 𝐵 ) → 𝐴 <s 𝐵 )
6 3 4 5 sltled ( ( 𝜑𝐴 <s 𝐵 ) → 𝐴 ≤s 𝐵 )
7 6 ex ( 𝜑 → ( 𝐴 <s 𝐵𝐴 ≤s 𝐵 ) )
8 sltne ( ( 𝐴 No 𝐴 <s 𝐵 ) → 𝐵𝐴 )
9 1 8 sylan ( ( 𝜑𝐴 <s 𝐵 ) → 𝐵𝐴 )
10 9 ex ( 𝜑 → ( 𝐴 <s 𝐵𝐵𝐴 ) )
11 7 10 jcad ( 𝜑 → ( 𝐴 <s 𝐵 → ( 𝐴 ≤s 𝐵𝐵𝐴 ) ) )
12 sleloe ( ( 𝐴 No 𝐵 No ) → ( 𝐴 ≤s 𝐵 ↔ ( 𝐴 <s 𝐵𝐴 = 𝐵 ) ) )
13 1 2 12 syl2anc ( 𝜑 → ( 𝐴 ≤s 𝐵 ↔ ( 𝐴 <s 𝐵𝐴 = 𝐵 ) ) )
14 eqneqall ( 𝐵 = 𝐴 → ( 𝐵𝐴𝐴 <s 𝐵 ) )
15 14 eqcoms ( 𝐴 = 𝐵 → ( 𝐵𝐴𝐴 <s 𝐵 ) )
16 15 jao1i ( ( 𝐴 <s 𝐵𝐴 = 𝐵 ) → ( 𝐵𝐴𝐴 <s 𝐵 ) )
17 13 16 biimtrdi ( 𝜑 → ( 𝐴 ≤s 𝐵 → ( 𝐵𝐴𝐴 <s 𝐵 ) ) )
18 17 impd ( 𝜑 → ( ( 𝐴 ≤s 𝐵𝐵𝐴 ) → 𝐴 <s 𝐵 ) )
19 11 18 impbid ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( 𝐴 ≤s 𝐵𝐵𝐴 ) ) )