sletric

Description: Surreal trichotomy law. (Contributed by Scott Fenton, 14-Feb-2025)

		Ref	Expression
	Assertion	sletric	$⊢ (A \in No \land B \in No) \to (A \leq_{s} B \lor B \leq_{s} A)$

Step	Hyp	Ref	Expression
1		sltasym	$⊢ (B \in No \land A \in No) \to (B <_{s} A \to \neg A <_{s} B)$
2		sltnle	$⊢ (B \in No \land A \in No) \to (B <_{s} A \leftrightarrow \neg A \leq_{s} B)$
3	2	bicomd	$⊢ (B \in No \land A \in No) \to (\neg A \leq_{s} B \leftrightarrow B <_{s} A)$
4		slenlt	$⊢ (B \in No \land A \in No) \to (B \leq_{s} A \leftrightarrow \neg A <_{s} B)$
5	1 3 4	3imtr4d	$⊢ (B \in No \land A \in No) \to (\neg A \leq_{s} B \to B \leq_{s} A)$
6	5	orrd	$⊢ (B \in No \land A \in No) \to (A \leq_{s} B \lor B \leq_{s} A)$
7	6	ancoms	$⊢ (A \in No \land B \in No) \to (A \leq_{s} B \lor B \leq_{s} A)$

Metamath Proof Explorer