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 ( 𝐴 ∈ No → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 bdayelon ⊢ ( bday ‘ 𝑥 ) ∈ On
2 1 onordi ⊢ Ord ( bday ‘ 𝑥 )
3 bdayelon ⊢ ( bday ‘ 𝐴 ) ∈ On
4 3 onordi ⊢ Ord ( bday ‘ 𝐴 )
5 ordtri2or ⊢ ( ( Ord ( bday ‘ 𝑥 ) ∧ Ord ( bday ‘ 𝐴 ) ) → ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ∨ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) ) )
6 2 4 5 mp2an ⊢ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ∨ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) )
7 6 a1i ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴 ) → ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ∨ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) ) )
8 madeun ⊢ ( M ‘ ( bday ‘ 𝑥 ) ) = ( ( O ‘ ( bday ‘ 𝑥 ) ) ∪ ( N ‘ ( bday ‘ 𝑥 ) ) )
9 8 eleq2i ⊢ ( 𝐴 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ↔ 𝐴 ∈ ( ( O ‘ ( bday ‘ 𝑥 ) ) ∪ ( N ‘ ( bday ‘ 𝑥 ) ) ) )
10 elun ⊢ ( 𝐴 ∈ ( ( O ‘ ( bday ‘ 𝑥 ) ) ∪ ( N ‘ ( bday ‘ 𝑥 ) ) ) ↔ ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∨ 𝐴 ∈ ( N ‘ ( bday ‘ 𝑥 ) ) ) )
11 9 10 bitri ⊢ ( 𝐴 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ↔ ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∨ 𝐴 ∈ ( N ‘ ( bday ‘ 𝑥 ) ) ) )
12 lrold ⊢ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) = ( O ‘ ( bday ‘ 𝑥 ) )
13 12 eleq2i ⊢ ( 𝐴 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ↔ 𝐴 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) )
14 elons ⊢ ( 𝑥 ∈ Ons ↔ ( 𝑥 ∈ No ∧ ( R ‘ 𝑥 ) = ∅ ) )
15 14 simprbi ⊢ ( 𝑥 ∈ Ons → ( R ‘ 𝑥 ) = ∅ )
16 15 adantl ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( R ‘ 𝑥 ) = ∅ )
17 16 uneq2d ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) = ( ( L ‘ 𝑥 ) ∪ ∅ ) )
18 un0 ⊢ ( ( L ‘ 𝑥 ) ∪ ∅ ) = ( L ‘ 𝑥 )
19 17 18 eqtrdi ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) = ( L ‘ 𝑥 ) )
20 19 eleq2d ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ↔ 𝐴 ∈ ( L ‘ 𝑥 ) ) )
21 simpll ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ 𝐴 ∈ ( L ‘ 𝑥 ) ) → 𝐴 ∈ No )
22 onsno ⊢ ( 𝑥 ∈ Ons → 𝑥 ∈ No )
23 22 ad2antlr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ 𝐴 ∈ ( L ‘ 𝑥 ) ) → 𝑥 ∈ No )
24 breq1 ⊢ ( 𝑥𝑂 = 𝐴 → ( 𝑥𝑂 <s 𝑥 ↔ 𝐴 <s 𝑥 ) )
25 leftval ⊢ ( L ‘ 𝑥 ) = { 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥𝑂 <s 𝑥 }
26 24 25 elrab2 ⊢ ( 𝐴 ∈ ( L ‘ 𝑥 ) ↔ ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∧ 𝐴 <s 𝑥 ) )
27 26 simprbi ⊢ ( 𝐴 ∈ ( L ‘ 𝑥 ) → 𝐴 <s 𝑥 )
28 27 adantl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ 𝐴 ∈ ( L ‘ 𝑥 ) ) → 𝐴 <s 𝑥 )
29 21 23 28 sltled ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ 𝐴 ∈ ( L ‘ 𝑥 ) ) → 𝐴 ≤s 𝑥 )
30 29 ex ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( L ‘ 𝑥 ) → 𝐴 ≤s 𝑥 ) )
31 20 30 sylbid ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) → 𝐴 ≤s 𝑥 ) )
32 13 31 biimtrrid ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) → 𝐴 ≤s 𝑥 ) )
33 newbday ⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ 𝐴 ∈ No ) → ( 𝐴 ∈ ( N ‘ ( bday ‘ 𝑥 ) ) ↔ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) )
34 1 33 mpan ⊢ ( 𝐴 ∈ No → ( 𝐴 ∈ ( N ‘ ( bday ‘ 𝑥 ) ) ↔ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) )
35 34 adantr ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( N ‘ ( bday ‘ 𝑥 ) ) ↔ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) )
36 leftssold ⊢ ( L ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) )
37 fveq2 ⊢ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) → ( O ‘ ( bday ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝑥 ) ) )
38 37 adantl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( O ‘ ( bday ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝑥 ) ) )
39 15 uneq2d ⊢ ( 𝑥 ∈ Ons → ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) = ( ( L ‘ 𝑥 ) ∪ ∅ ) )
40 39 12 18 3eqtr3g ⊢ ( 𝑥 ∈ Ons → ( O ‘ ( bday ‘ 𝑥 ) ) = ( L ‘ 𝑥 ) )
41 40 ad2antlr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( O ‘ ( bday ‘ 𝑥 ) ) = ( L ‘ 𝑥 ) )
42 38 41 eqtr2d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( L ‘ 𝑥 ) = ( O ‘ ( bday ‘ 𝐴 ) ) )
43 36 42 sseqtrrid ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( L ‘ 𝐴 ) ⊆ ( L ‘ 𝑥 ) )
44 slelss ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ No ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( 𝐴 ≤s 𝑥 ↔ ( L ‘ 𝐴 ) ⊆ ( L ‘ 𝑥 ) ) )
45 22 44 syl3an2 ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( 𝐴 ≤s 𝑥 ↔ ( L ‘ 𝐴 ) ⊆ ( L ‘ 𝑥 ) ) )
46 45 3expa ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( 𝐴 ≤s 𝑥 ↔ ( L ‘ 𝐴 ) ⊆ ( L ‘ 𝑥 ) ) )
47 43 46 mpbird ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → 𝐴 ≤s 𝑥 )
48 47 ex ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) → 𝐴 ≤s 𝑥 ) )
49 35 48 sylbid ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( N ‘ ( bday ‘ 𝑥 ) ) → 𝐴 ≤s 𝑥 ) )
50 32 49 jaod ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∨ 𝐴 ∈ ( N ‘ ( bday ‘ 𝑥 ) ) ) → 𝐴 ≤s 𝑥 ) )
51 11 50 biimtrid ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) → 𝐴 ≤s 𝑥 ) )
52 madebday ⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ 𝐴 ∈ No ) → ( 𝐴 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ↔ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) ) )
53 1 52 mpan ⊢ ( 𝐴 ∈ No → ( 𝐴 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ↔ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) ) )
54 53 adantr ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ↔ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) ) )
55 slenlt ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ No ) → ( 𝐴 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝐴 ) )
56 22 55 sylan2 ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝐴 ) )
57 51 54 56 3imtr3d ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) → ¬ 𝑥 <s 𝐴 ) )
58 57 con2d ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝑥 <s 𝐴 → ¬ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) ) )
59 58 3impia ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴 ) → ¬ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) )
60 7 59 olcnd ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴 ) → ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) )
61 22 3ad2ant2 ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴 ) → 𝑥 ∈ No )
62 oldbday ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ 𝑥 ∈ No ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ) )
63 3 61 62 sylancr ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴 ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ) )
64 60 63 mpbird ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴 ) → 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
65 64 rabssdv ⊢ ( 𝐴 ∈ No → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) )