Theorem lesid

Description: Surreal less-than or equal is reflexive. Theorem 0(iii) of Conway p. 16. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	lesid	$$⊢A\in \mathrm{No}\to A{\le }_{s}A$$

Proof

Step	Hyp	Ref	Expression
1		ltsirr	$$⊢A\in \mathrm{No}\to \neg A{<}_{s}A$$
2		lenlts	$$⊢\left(A\in \mathrm{No}\wedge A\in \mathrm{No}\right)\to \left(A{\le }_{s}A\leftrightarrow \neg A{<}_{s}A\right)$$
3	2	anidms	$$⊢A\in \mathrm{No}\to \left(A{\le }_{s}A\leftrightarrow \neg A{<}_{s}A\right)$$
4	1 3	mpbird	$$⊢A\in \mathrm{No}\to A{\le }_{s}A$$