sltlend

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

	Ref	Expression
Hypotheses	sltlen.1	$⊢ φ \to A \in No$
	sltlen.2	$⊢ φ \to B \in No$
Assertion	sltlend	$⊢ φ \to (A <_{s} B \leftrightarrow (A \leq_{s} B \land B \neq A))$

Step	Hyp	Ref	Expression
1		sltlen.1	$⊢ φ \to A \in No$
2		sltlen.2	$⊢ φ \to B \in No$
3	1	adantr	$⊢ (φ \land A <_{s} B) \to A \in No$
4	2	adantr	$⊢ (φ \land A <_{s} B) \to B \in No$
5		simpr	$⊢ (φ \land A <_{s} B) \to A <_{s} B$
6	3 4 5	sltled	$⊢ (φ \land A <_{s} B) \to A \leq_{s} B$
7	6	ex	$⊢ φ \to (A <_{s} B \to A \leq_{s} B)$
8		sltne	$⊢ (A \in No \land A <_{s} B) \to B \neq A$
9	1 8	sylan	$⊢ (φ \land A <_{s} B) \to B \neq A$
10	9	ex	$⊢ φ \to (A <_{s} B \to B \neq A)$
11	7 10	jcad	$⊢ φ \to (A <_{s} B \to (A \leq_{s} B \land B \neq A))$
12		sleloe	$⊢ (A \in No \land B \in No) \to (A \leq_{s} B \leftrightarrow (A <_{s} B \lor A = B))$
13	1 2 12	syl2anc	$⊢ φ \to (A \leq_{s} B \leftrightarrow (A <_{s} B \lor A = B))$
14		eqneqall	$⊢ B = A \to (B \neq A \to A <_{s} B)$
15	14	eqcoms	$⊢ A = B \to (B \neq A \to A <_{s} B)$
16	15	jao1i	$⊢ (A <_{s} B \lor A = B) \to (B \neq A \to A <_{s} B)$
17	13 16	biimtrdi	$⊢ φ \to (A \leq_{s} B \to (B \neq A \to A <_{s} B))$
18	17	impd	$⊢ φ \to ((A \leq_{s} B \land B \neq A) \to A <_{s} B)$
19	11 18	impbid	$⊢ φ \to (A <_{s} B \leftrightarrow (A \leq_{s} B \land B \neq A))$

Metamath Proof Explorer