Theorem sltonold

Description: The class of ordinals less than any surreal is a subset of that surreal's old set. (Contributed by Scott Fenton, 22-Mar-2025)

	Ref	Expression
Assertion	sltonold	|- ( A e. No -> { x e. On_s | x

Proof

Step	Hyp	Ref	Expression
1		bdayelon	|- ( bday ` x ) e. On
2	1	onordi	|- Ord ( bday ` x )
3		bdayelon	|- ( bday ` A ) e. On
4	3	onordi	|- Ord ( bday ` A )
5		ordtri2or	|- ( ( Ord ( bday ` x ) /\ Ord ( bday ` A ) ) -> ( ( bday ` x ) e. ( bday ` A ) \/ ( bday ` A ) C_ ( bday ` x ) ) )
6	2 4 5	mp2an	|- ( ( bday ` x ) e. ( bday ` A ) \/ ( bday ` A ) C_ ( bday ` x ) )
7	6	a1i	|- ( ( A e. No /\ x e. On_s /\ x ( ( bday ` x ) e. ( bday ` A ) \/ ( bday ` A ) C_ ( bday ` x ) ) )
8		madeun	|- ( _Made ` ( bday ` x ) ) = ( ( _Old ` ( bday ` x ) ) u. ( _New ` ( bday ` x ) ) )
9	8	eleq2i	|- ( A e. ( _Made ` ( bday ` x ) ) <-> A e. ( ( _Old ` ( bday ` x ) ) u. ( _New ` ( bday ` x ) ) ) )
10		elun	|- ( A e. ( ( _Old ` ( bday ` x ) ) u. ( _New ` ( bday ` x ) ) ) <-> ( A e. ( _Old ` ( bday ` x ) ) \/ A e. ( _New ` ( bday ` x ) ) ) )
11	9 10	bitri	|- ( A e. ( _Made ` ( bday ` x ) ) <-> ( A e. ( _Old ` ( bday ` x ) ) \/ A e. ( _New ` ( bday ` x ) ) ) )
12		lrold	|- ( ( _Left ` x ) u. ( _Right ` x ) ) = ( _Old ` ( bday ` x ) )
13	12	eleq2i	|- ( A e. ( ( _Left ` x ) u. ( _Right ` x ) ) <-> A e. ( _Old ` ( bday ` x ) ) )
14		elons	|- ( x e. On_s <-> ( x e. No /\ ( _Right ` x ) = (/) ) )
15	14	simprbi	|- ( x e. On_s -> ( _Right ` x ) = (/) )
16	15	adantl	|- ( ( A e. No /\ x e. On_s ) -> ( _Right ` x ) = (/) )
17	16	uneq2d	|- ( ( A e. No /\ x e. On_s ) -> ( ( _Left ` x ) u. ( _Right ` x ) ) = ( ( _Left ` x ) u. (/) ) )
18		un0	|- ( ( _Left ` x ) u. (/) ) = ( _Left ` x )
19	17 18	eqtrdi	|- ( ( A e. No /\ x e. On_s ) -> ( ( _Left ` x ) u. ( _Right ` x ) ) = ( _Left ` x ) )
20	19	eleq2d	|- ( ( A e. No /\ x e. On_s ) -> ( A e. ( ( _Left ` x ) u. ( _Right ` x ) ) <-> A e. ( _Left ` x ) ) )
21		simpll	|- ( ( ( A e. No /\ x e. On_s ) /\ A e. ( _Left ` x ) ) -> A e. No )
22		onsno	|- ( x e. On_s -> x e. No )
23	22	ad2antlr	|- ( ( ( A e. No /\ x e. On_s ) /\ A e. ( _Left ` x ) ) -> x e. No )
24		breq1	|- ( xO = A -> ( xO A
25		leftval	|- ( _Left ` x ) = { xO e. ( _Old ` ( bday ` x ) ) | xO
26	24 25	elrab2	|- ( A e. ( _Left ` x ) <-> ( A e. ( _Old ` ( bday ` x ) ) /\ A
27	26	simprbi	|- ( A e. ( _Left ` x ) -> A
28	27	adantl	|- ( ( ( A e. No /\ x e. On_s ) /\ A e. ( _Left ` x ) ) -> A
29	21 23 28	sltled	|- ( ( ( A e. No /\ x e. On_s ) /\ A e. ( _Left ` x ) ) -> A <_s x )
30	29	ex	|- ( ( A e. No /\ x e. On_s ) -> ( A e. ( _Left ` x ) -> A <_s x ) )
31	20 30	sylbid	|- ( ( A e. No /\ x e. On_s ) -> ( A e. ( ( _Left ` x ) u. ( _Right ` x ) ) -> A <_s x ) )
32	13 31	biimtrrid	|- ( ( A e. No /\ x e. On_s ) -> ( A e. ( _Old ` ( bday ` x ) ) -> A <_s x ) )
33		newbday	|- ( ( ( bday ` x ) e. On /\ A e. No ) -> ( A e. ( _New ` ( bday ` x ) ) <-> ( bday ` A ) = ( bday ` x ) ) )
34	1 33	mpan	|- ( A e. No -> ( A e. ( _New ` ( bday ` x ) ) <-> ( bday ` A ) = ( bday ` x ) ) )
35	34	adantr	|- ( ( A e. No /\ x e. On_s ) -> ( A e. ( _New ` ( bday ` x ) ) <-> ( bday ` A ) = ( bday ` x ) ) )
36		leftssold	|- ( _Left ` A ) C_ ( _Old ` ( bday ` A ) )
37		fveq2	|- ( ( bday ` A ) = ( bday ` x ) -> ( _Old ` ( bday ` A ) ) = ( _Old ` ( bday ` x ) ) )
38	37	adantl	|- ( ( ( A e. No /\ x e. On_s ) /\ ( bday ` A ) = ( bday ` x ) ) -> ( _Old ` ( bday ` A ) ) = ( _Old ` ( bday ` x ) ) )
39	15	uneq2d	|- ( x e. On_s -> ( ( _Left ` x ) u. ( _Right ` x ) ) = ( ( _Left ` x ) u. (/) ) )
40	39 12 18	3eqtr3g	|- ( x e. On_s -> ( _Old ` ( bday ` x ) ) = ( _Left ` x ) )
41	40	ad2antlr	|- ( ( ( A e. No /\ x e. On_s ) /\ ( bday ` A ) = ( bday ` x ) ) -> ( _Old ` ( bday ` x ) ) = ( _Left ` x ) )
42	38 41	eqtr2d	|- ( ( ( A e. No /\ x e. On_s ) /\ ( bday ` A ) = ( bday ` x ) ) -> ( _Left ` x ) = ( _Old ` ( bday ` A ) ) )
43	36 42	sseqtrrid	|- ( ( ( A e. No /\ x e. On_s ) /\ ( bday ` A ) = ( bday ` x ) ) -> ( _Left ` A ) C_ ( _Left ` x ) )
44		slelss	|- ( ( A e. No /\ x e. No /\ ( bday ` A ) = ( bday ` x ) ) -> ( A <_s x <-> ( _Left ` A ) C_ ( _Left ` x ) ) )
45	22 44	syl3an2	|- ( ( A e. No /\ x e. On_s /\ ( bday ` A ) = ( bday ` x ) ) -> ( A <_s x <-> ( _Left ` A ) C_ ( _Left ` x ) ) )
46	45	3expa	|- ( ( ( A e. No /\ x e. On_s ) /\ ( bday ` A ) = ( bday ` x ) ) -> ( A <_s x <-> ( _Left ` A ) C_ ( _Left ` x ) ) )
47	43 46	mpbird	|- ( ( ( A e. No /\ x e. On_s ) /\ ( bday ` A ) = ( bday ` x ) ) -> A <_s x )
48	47	ex	|- ( ( A e. No /\ x e. On_s ) -> ( ( bday ` A ) = ( bday ` x ) -> A <_s x ) )
49	35 48	sylbid	|- ( ( A e. No /\ x e. On_s ) -> ( A e. ( _New ` ( bday ` x ) ) -> A <_s x ) )
50	32 49	jaod	|- ( ( A e. No /\ x e. On_s ) -> ( ( A e. ( _Old ` ( bday ` x ) ) \/ A e. ( _New ` ( bday ` x ) ) ) -> A <_s x ) )
51	11 50	biimtrid	|- ( ( A e. No /\ x e. On_s ) -> ( A e. ( _Made ` ( bday ` x ) ) -> A <_s x ) )
52		madebday	|- ( ( ( bday ` x ) e. On /\ A e. No ) -> ( A e. ( _Made ` ( bday ` x ) ) <-> ( bday ` A ) C_ ( bday ` x ) ) )
53	1 52	mpan	|- ( A e. No -> ( A e. ( _Made ` ( bday ` x ) ) <-> ( bday ` A ) C_ ( bday ` x ) ) )
54	53	adantr	|- ( ( A e. No /\ x e. On_s ) -> ( A e. ( _Made ` ( bday ` x ) ) <-> ( bday ` A ) C_ ( bday ` x ) ) )
55		slenlt	|- ( ( A e. No /\ x e. No ) -> ( A <_s x <-> -. x
56	22 55	sylan2	|- ( ( A e. No /\ x e. On_s ) -> ( A <_s x <-> -. x
57	51 54 56	3imtr3d	|- ( ( A e. No /\ x e. On_s ) -> ( ( bday ` A ) C_ ( bday ` x ) -> -. x
58	57	con2d	|- ( ( A e. No /\ x e. On_s ) -> ( x -. ( bday ` A ) C_ ( bday ` x ) ) )
59	58	3impia	|- ( ( A e. No /\ x e. On_s /\ x -. ( bday ` A ) C_ ( bday ` x ) )
60	7 59	olcnd	|- ( ( A e. No /\ x e. On_s /\ x ( bday ` x ) e. ( bday ` A ) )
61	22	3ad2ant2	|- ( ( A e. No /\ x e. On_s /\ x x e. No )
62		oldbday	|- ( ( ( bday ` A ) e. On /\ x e. No ) -> ( x e. ( _Old ` ( bday ` A ) ) <-> ( bday ` x ) e. ( bday ` A ) ) )
63	3 61 62	sylancr	|- ( ( A e. No /\ x e. On_s /\ x ( x e. ( _Old ` ( bday ` A ) ) <-> ( bday ` x ) e. ( bday ` A ) ) )
64	60 63	mpbird	|- ( ( A e. No /\ x e. On_s /\ x x e. ( _Old ` ( bday ` A ) ) )
65	64	rabssdv	|- ( A e. No -> { x e. On_s | x