Metamath Proof Explorer

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 leftlt 
 |-  ( A e. ( _Left ` x ) -> A
25 24 adantl 
 |-  ( ( ( A e. No /\ x e. On_s ) /\ A e. ( _Left ` x ) ) -> A
26 21 23 25 sltled 
 |-  ( ( ( A e. No /\ x e. On_s ) /\ A e. ( _Left ` x ) ) -> A <_s x )
27 26 ex 
 |-  ( ( A e. No /\ x e. On_s ) -> ( A e. ( _Left ` x ) -> A <_s x ) )
28 20 27 sylbid 
 |-  ( ( A e. No /\ x e. On_s ) -> ( A e. ( ( _Left ` x ) u. ( _Right ` x ) ) -> A <_s x ) )
29 13 28 biimtrrid 
 |-  ( ( A e. No /\ x e. On_s ) -> ( A e. ( _Old ` ( bday ` x ) ) -> A <_s x ) )
30 newbday 
 |-  ( ( ( bday ` x ) e. On /\ A e. No ) -> ( A e. ( _New ` ( bday ` x ) ) <-> ( bday ` A ) = ( bday ` x ) ) )
31 1 30 mpan 
 |-  ( A e. No -> ( A e. ( _New ` ( bday ` x ) ) <-> ( bday ` A ) = ( bday ` x ) ) )
32 31 adantr 
 |-  ( ( A e. No /\ x e. On_s ) -> ( A e. ( _New ` ( bday ` x ) ) <-> ( bday ` A ) = ( bday ` x ) ) )
33 leftssold 
 |-  ( _Left ` A ) C_ ( _Old ` ( bday ` A ) )
34 fveq2 
 |-  ( ( bday ` A ) = ( bday ` x ) -> ( _Old ` ( bday ` A ) ) = ( _Old ` ( bday ` x ) ) )
35 34 adantl 
 |-  ( ( ( A e. No /\ x e. On_s ) /\ ( bday ` A ) = ( bday ` x ) ) -> ( _Old ` ( bday ` A ) ) = ( _Old ` ( bday ` x ) ) )
36 onsleft 
 |-  ( x e. On_s -> ( _Old ` ( bday ` x ) ) = ( _Left ` x ) )
37 36 ad2antlr 
 |-  ( ( ( A e. No /\ x e. On_s ) /\ ( bday ` A ) = ( bday ` x ) ) -> ( _Old ` ( bday ` x ) ) = ( _Left ` x ) )
38 35 37 eqtr2d 
 |-  ( ( ( A e. No /\ x e. On_s ) /\ ( bday ` A ) = ( bday ` x ) ) -> ( _Left ` x ) = ( _Old ` ( bday ` A ) ) )
39 33 38 sseqtrrid 
 |-  ( ( ( A e. No /\ x e. On_s ) /\ ( bday ` A ) = ( bday ` x ) ) -> ( _Left ` A ) C_ ( _Left ` x ) )
40 slelss 
 |-  ( ( A e. No /\ x e. No /\ ( bday ` A ) = ( bday ` x ) ) -> ( A <_s x <-> ( _Left ` A ) C_ ( _Left ` x ) ) )
41 22 40 syl3an2 
 |-  ( ( A e. No /\ x e. On_s /\ ( bday ` A ) = ( bday ` x ) ) -> ( A <_s x <-> ( _Left ` A ) C_ ( _Left ` x ) ) )
42 41 3expa 
 |-  ( ( ( A e. No /\ x e. On_s ) /\ ( bday ` A ) = ( bday ` x ) ) -> ( A <_s x <-> ( _Left ` A ) C_ ( _Left ` x ) ) )
43 39 42 mpbird 
 |-  ( ( ( A e. No /\ x e. On_s ) /\ ( bday ` A ) = ( bday ` x ) ) -> A <_s x )
44 43 ex 
 |-  ( ( A e. No /\ x e. On_s ) -> ( ( bday ` A ) = ( bday ` x ) -> A <_s x ) )
45 32 44 sylbid 
 |-  ( ( A e. No /\ x e. On_s ) -> ( A e. ( _New ` ( bday ` x ) ) -> A <_s x ) )
46 29 45 jaod 
 |-  ( ( A e. No /\ x e. On_s ) -> ( ( A e. ( _Old ` ( bday ` x ) ) \/ A e. ( _New ` ( bday ` x ) ) ) -> A <_s x ) )
47 11 46 biimtrid 
 |-  ( ( A e. No /\ x e. On_s ) -> ( A e. ( _Made ` ( bday ` x ) ) -> A <_s x ) )
48 madebday 
 |-  ( ( ( bday ` x ) e. On /\ A e. No ) -> ( A e. ( _Made ` ( bday ` x ) ) <-> ( bday ` A ) C_ ( bday ` x ) ) )
49 1 48 mpan 
 |-  ( A e. No -> ( A e. ( _Made ` ( bday ` x ) ) <-> ( bday ` A ) C_ ( bday ` x ) ) )
50 49 adantr 
 |-  ( ( A e. No /\ x e. On_s ) -> ( A e. ( _Made ` ( bday ` x ) ) <-> ( bday ` A ) C_ ( bday ` x ) ) )
51 slenlt 
 |-  ( ( A e. No /\ x e. No ) -> ( A <_s x <-> -. x
52 22 51 sylan2 
 |-  ( ( A e. No /\ x e. On_s ) -> ( A <_s x <-> -. x
53 47 50 52 3imtr3d 
 |-  ( ( A e. No /\ x e. On_s ) -> ( ( bday ` A ) C_ ( bday ` x ) -> -. x
54 53 con2d 
 |-  ( ( A e. No /\ x e. On_s ) -> ( x  -. ( bday ` A ) C_ ( bday ` x ) ) )
55 54 3impia 
 |-  ( ( A e. No /\ x e. On_s /\ x  -. ( bday ` A ) C_ ( bday ` x ) )
56 7 55 olcnd 
 |-  ( ( A e. No /\ x e. On_s /\ x  ( bday ` x ) e. ( bday ` A ) )
57 22 3ad2ant2 
 |-  ( ( A e. No /\ x e. On_s /\ x  x e. No )
58 oldbday 
 |-  ( ( ( bday ` A ) e. On /\ x e. No ) -> ( x e. ( _Old ` ( bday ` A ) ) <-> ( bday ` x ) e. ( bday ` A ) ) )
59 3 57 58 sylancr 
 |-  ( ( A e. No /\ x e. On_s /\ x  ( x e. ( _Old ` ( bday ` A ) ) <-> ( bday ` x ) e. ( bday ` A ) ) )
60 56 59 mpbird 
 |-  ( ( A e. No /\ x e. On_s /\ x  x e. ( _Old ` ( bday ` A ) ) )
61 60 rabssdv 
 |-  ( A e. No -> { x e. On_s | x