Theorem sleloe

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

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

Proof

Step	Hyp	Ref	Expression
1		slenlt	|- ( ( A e. No /\ B e. No ) -> ( A <_s B <-> -. B
2		orcom	|- ( ( A ( A = B \/ A
3		eqcom	|- ( A = B <-> B = A )
4	3	orbi1i	|- ( ( A = B \/ A ( B = A \/ A
5	2 4	bitri	|- ( ( A ( B = A \/ A
6		sltso	|-
7		sotric	|- ( ( ( B -. ( B = A \/ A
8	6 7	mpan	|- ( ( B e. No /\ A e. No ) -> ( B -. ( B = A \/ A
9	8	ancoms	|- ( ( A e. No /\ B e. No ) -> ( B -. ( B = A \/ A
10	9	con2bid	|- ( ( A e. No /\ B e. No ) -> ( ( B = A \/ A -. B
11	5 10	bitrid	|- ( ( A e. No /\ B e. No ) -> ( ( A -. B
12	1 11	bitr4d	|- ( ( A e. No /\ B e. No ) -> ( A <_s B <-> ( A