Metamath Proof Explorer

Theorem ltonold

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

Proof

Step Hyp Ref Expression
1 bdayon ⊢ ( bday ‘ 𝑥 ) ∈ On
2 1 onordi ⊢ Ord ( bday ‘ 𝑥 )
3 bdayon ⊢ ( 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 onno ⊢ ( 𝑥 ∈ Ons → 𝑥 ∈ No )
23 22 ad2antlr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ 𝐴 ∈ ( L ‘ 𝑥 ) ) → 𝑥 ∈ No )
24 leftlt ⊢ ( 𝐴 ∈ ( L ‘ 𝑥 ) → 𝐴 <s 𝑥 )
25 24 adantl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ 𝐴 ∈ ( L ‘ 𝑥 ) ) → 𝐴 <s 𝑥 )
26 21 23 25 ltlesd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ 𝐴 ∈ ( L ‘ 𝑥 ) ) → 𝐴 ≤s 𝑥 )
27 26 ex ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( L ‘ 𝑥 ) → 𝐴 ≤s 𝑥 ) )
28 20 27 sylbid ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) → 𝐴 ≤s 𝑥 ) )
29 13 28 biimtrrid ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) → 𝐴 ≤s 𝑥 ) )
30 newbday ⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ 𝐴 ∈ No ) → ( 𝐴 ∈ ( N ‘ ( bday ‘ 𝑥 ) ) ↔ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) )
31 1 30 mpan ⊢ ( 𝐴 ∈ No → ( 𝐴 ∈ ( N ‘ ( bday ‘ 𝑥 ) ) ↔ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) )
32 31 adantr ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( N ‘ ( bday ‘ 𝑥 ) ) ↔ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) )
33 leftssold ⊢ ( L ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) )
34 fveq2 ⊢ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) → ( O ‘ ( bday ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝑥 ) ) )
35 34 adantl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( O ‘ ( bday ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝑥 ) ) )
36 onleft ⊢ ( 𝑥 ∈ Ons → ( O ‘ ( bday ‘ 𝑥 ) ) = ( L ‘ 𝑥 ) )
37 36 ad2antlr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( O ‘ ( bday ‘ 𝑥 ) ) = ( L ‘ 𝑥 ) )
38 35 37 eqtr2d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( L ‘ 𝑥 ) = ( O ‘ ( bday ‘ 𝐴 ) ) )
39 33 38 sseqtrrid ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( L ‘ 𝐴 ) ⊆ ( L ‘ 𝑥 ) )
40 leslss ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ No ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( 𝐴 ≤s 𝑥 ↔ ( L ‘ 𝐴 ) ⊆ ( L ‘ 𝑥 ) ) )
41 22 40 syl3an2 ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( 𝐴 ≤s 𝑥 ↔ ( L ‘ 𝐴 ) ⊆ ( L ‘ 𝑥 ) ) )
42 41 3expa ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → ( 𝐴 ≤s 𝑥 ↔ ( L ‘ 𝐴 ) ⊆ ( L ‘ 𝑥 ) ) )
43 39 42 mpbird ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) ) → 𝐴 ≤s 𝑥 )
44 43 ex ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝑥 ) → 𝐴 ≤s 𝑥 ) )
45 32 44 sylbid ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( N ‘ ( bday ‘ 𝑥 ) ) → 𝐴 ≤s 𝑥 ) )
46 29 45 jaod ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∨ 𝐴 ∈ ( N ‘ ( bday ‘ 𝑥 ) ) ) → 𝐴 ≤s 𝑥 ) )
47 11 46 biimtrid ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) → 𝐴 ≤s 𝑥 ) )
48 madebday ⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ 𝐴 ∈ No ) → ( 𝐴 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ↔ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) ) )
49 1 48 mpan ⊢ ( 𝐴 ∈ No → ( 𝐴 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ↔ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) ) )
50 49 adantr ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ↔ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) ) )
51 lenlts ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ No ) → ( 𝐴 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝐴 ) )
52 22 51 sylan2 ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝐴 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝐴 ) )
53 47 50 52 3imtr3d ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) → ¬ 𝑥 <s 𝐴 ) )
54 53 con2d ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ) → ( 𝑥 <s 𝐴 → ¬ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) ) )
55 54 3impia ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴 ) → ¬ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑥 ) )
56 7 55 olcnd ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴 ) → ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) )
57 22 3ad2ant2 ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴 ) → 𝑥 ∈ No )
58 oldbday ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ 𝑥 ∈ No ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ) )
59 3 57 58 sylancr ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴 ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ) )
60 56 59 mpbird ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴 ) → 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
61 60 rabssdv ⊢ ( 𝐴 ∈ No → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) )