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	⊢ ( 𝜑 → 𝐴 ∈ No )
	ltlesn.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	ltlesnd	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( 𝐴 ≤s 𝐵 ∧ 𝐵 ≠ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltlesn.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		ltlesn.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 <s 𝐵 ) → 𝐴 ∈ No )
4	2	adantr	⊢ ( ( 𝜑 ∧ 𝐴 <s 𝐵 ) → 𝐵 ∈ No )
5		simpr	⊢ ( ( 𝜑 ∧ 𝐴 <s 𝐵 ) → 𝐴 <s 𝐵 )
6	3 4 5	ltlesd	⊢ ( ( 𝜑 ∧ 𝐴 <s 𝐵 ) → 𝐴 ≤s 𝐵 )
7	6	ex	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 → 𝐴 ≤s 𝐵 ) )
8		ltsne	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 <s 𝐵 ) → 𝐵 ≠ 𝐴 )
9	1 8	sylan	⊢ ( ( 𝜑 ∧ 𝐴 <s 𝐵 ) → 𝐵 ≠ 𝐴 )
10	9	ex	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 → 𝐵 ≠ 𝐴 ) )
11	7 10	jcad	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 → ( 𝐴 ≤s 𝐵 ∧ 𝐵 ≠ 𝐴 ) ) )
12		lesloe	⊢ ( ( 𝐴 ∈ 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 𝐵 ∧ 𝐵 ≠ 𝐴 ) ) )