sleloe

Description: Surreal less-than or equal in terms of less-than. (Contributed by Scott Fenton, 8-Dec-2021)

		Ref	Expression
	Assertion	sleloe	$⊢ (A \in No \land B \in No) \to (A \leq_{s} B \leftrightarrow (A <_{s} B \lor A = B))$

Step	Hyp	Ref	Expression
1		slenlt	$⊢ (A \in No \land B \in No) \to (A \leq_{s} B \leftrightarrow \neg B <_{s} A)$
2		orcom	$⊢ (A <_{s} B \lor A = B) \leftrightarrow (A = B \lor A <_{s} B)$
3		eqcom	$⊢ A = B \leftrightarrow B = A$
4	3	orbi1i	$⊢ (A = B \lor A <_{s} B) \leftrightarrow (B = A \lor A <_{s} B)$
5	2 4	bitri	$⊢ (A <_{s} B \lor A = B) \leftrightarrow (B = A \lor A <_{s} B)$
6		sltso	$⊢ <_{s} Or No$
7		sotric	$⊢ (<_{s} Or No \land (B \in No \land A \in No)) \to (B <_{s} A \leftrightarrow \neg (B = A \lor A <_{s} B))$
8	6 7	mpan	$⊢ (B \in No \land A \in No) \to (B <_{s} A \leftrightarrow \neg (B = A \lor A <_{s} B))$
9	8	ancoms	$⊢ (A \in No \land B \in No) \to (B <_{s} A \leftrightarrow \neg (B = A \lor A <_{s} B))$
10	9	con2bid	$⊢ (A \in No \land B \in No) \to ((B = A \lor A <_{s} B) \leftrightarrow \neg B <_{s} A)$
11	5 10	bitrid	$⊢ (A \in No \land B \in No) \to ((A <_{s} B \lor A = B) \leftrightarrow \neg B <_{s} A)$
12	1 11	bitr4d	$⊢ (A \in No \land B \in No) \to (A \leq_{s} B \leftrightarrow (A <_{s} B \lor A = B))$

Metamath Proof Explorer