Theorem sltled

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

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

Proof

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