Theorem ltlesd

Description: Surreal less-than implies less-than or equal. (Contributed by Scott Fenton, 16-Feb-2025)

	Ref	Expression
Hypotheses	ltlesd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	ltlesd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	ltlesd.3	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
Assertion	ltlesd	⊢ ( 𝜑 → 𝐴 ≤s 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ltlesd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		ltlesd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		ltlesd.3	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
4	1 2	jca	⊢ ( 𝜑 → ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) )
5		ltsasym	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 → ¬ 𝐵 <s 𝐴 ) )
6	4 3 5	sylc	⊢ ( 𝜑 → ¬ 𝐵 <s 𝐴 )
7		lenlts	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴 ) )
8	1 2 7	syl2anc	⊢ ( 𝜑 → ( 𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴 ) )
9	6 8	mpbird	⊢ ( 𝜑 → 𝐴 ≤s 𝐵 )