Theorem onslt

Description: Less-than is the same as birthday comparison over surreal ordinals. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Assertion	onslt	|- ( ( A e. On_s /\ B e. On_s ) -> ( A ( bday ` A ) e. ( bday ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		onsno	|- ( B e. On_s -> B e. No )
2		onnolt	|- ( ( A e. On_s /\ B e. No /\ A ( bday ` A ) e. ( bday ` B ) )
3	2	3expia	|- ( ( A e. On_s /\ B e. No ) -> ( A ( bday ` A ) e. ( bday ` B ) ) )
4	1 3	sylan2	|- ( ( A e. On_s /\ B e. On_s ) -> ( A ( bday ` A ) e. ( bday ` B ) ) )
5		bdayelon	|- ( bday ` B ) e. On
6		onsno	|- ( A e. On_s -> A e. No )
7	6	adantr	|- ( ( A e. On_s /\ B e. On_s ) -> A e. No )
8		oldbday	|- ( ( ( bday ` B ) e. On /\ A e. No ) -> ( A e. ( _Old ` ( bday ` B ) ) <-> ( bday ` A ) e. ( bday ` B ) ) )
9	5 7 8	sylancr	|- ( ( A e. On_s /\ B e. On_s ) -> ( A e. ( _Old ` ( bday ` B ) ) <-> ( bday ` A ) e. ( bday ` B ) ) )
10		onsleft	|- ( B e. On_s -> ( _Old ` ( bday ` B ) ) = ( _Left ` B ) )
11	10	eleq2d	|- ( B e. On_s -> ( A e. ( _Old ` ( bday ` B ) ) <-> A e. ( _Left ` B ) ) )
12	11	adantl	|- ( ( A e. On_s /\ B e. On_s ) -> ( A e. ( _Old ` ( bday ` B ) ) <-> A e. ( _Left ` B ) ) )
13	9 12	bitr3d	|- ( ( A e. On_s /\ B e. On_s ) -> ( ( bday ` A ) e. ( bday ` B ) <-> A e. ( _Left ` B ) ) )
14		leftlt	|- ( A e. ( _Left ` B ) -> A
15	13 14	biimtrdi	|- ( ( A e. On_s /\ B e. On_s ) -> ( ( bday ` A ) e. ( bday ` B ) -> A
16	4 15	impbid	|- ( ( A e. On_s /\ B e. On_s ) -> ( A ( bday ` A ) e. ( bday ` B ) ) )