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 ∈ No → x ∈ On s | x < s A ⊆ Old ⁡ bday ⁡ A

Proof

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