Theorem sletric

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

	Ref	Expression
Assertion	sletric	|- ( ( A e. No /\ B e. No ) -> ( A <_s B \/ B <_s A ) )

Proof

Step	Hyp	Ref	Expression
1		sltasym	|- ( ( B e. No /\ A e. No ) -> ( B -. A
2		sltnle	|- ( ( B e. No /\ A e. No ) -> ( B -. A <_s B ) )
3	2	bicomd	|- ( ( B e. No /\ A e. No ) -> ( -. A <_s B <-> B
4		slenlt	|- ( ( B e. No /\ A e. No ) -> ( B <_s A <-> -. A
5	1 3 4	3imtr4d	|- ( ( B e. No /\ A e. No ) -> ( -. A <_s B -> B <_s A ) )
6	5	orrd	|- ( ( B e. No /\ A e. No ) -> ( A <_s B \/ B <_s A ) )
7	6	ancoms	|- ( ( A e. No /\ B e. No ) -> ( A <_s B \/ B <_s A ) )