Theorem slenlt

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

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

Proof

Step	Hyp	Ref	Expression
1		df-sle	|- <_s = ( ( No X. No ) \ `'
2	1	breqi	|- ( A <_s B <-> A ( ( No X. No ) \ `'
3		brdif	|- ( A ( ( No X. No ) \ `' ( A ( No X. No ) B /\ -. A `'
4		brxp	|- ( A ( No X. No ) B <-> ( A e. No /\ B e. No ) )
5	4	anbi1i	|- ( ( A ( No X. No ) B /\ -. A `' ( ( A e. No /\ B e. No ) /\ -. A `'
6	2 3 5	3bitri	|- ( A <_s B <-> ( ( A e. No /\ B e. No ) /\ -. A `'
7		ibar	|- ( ( A e. No /\ B e. No ) -> ( -. A `' ( ( A e. No /\ B e. No ) /\ -. A `'
8		brcnvg	|- ( ( A e. No /\ B e. No ) -> ( A `' B
9	8	notbid	|- ( ( A e. No /\ B e. No ) -> ( -. A `' -. B
10	7 9	bitr3d	|- ( ( A e. No /\ B e. No ) -> ( ( ( A e. No /\ B e. No ) /\ -. A `' -. B
11	6 10	syl5bb	|- ( ( A e. No /\ B e. No ) -> ( A <_s B <-> -. B