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 leftlt ⊢ A ∈ L ⁡ x → A < s x
25 24 adantl ⊢ A ∈ No ∧ x ∈ On s ∧ A ∈ L ⁡ x → A < s x
26 21 23 25 sltled ⊢ A ∈ No ∧ x ∈ On s ∧ A ∈ L ⁡ x → A ≤ s x
27 26 ex ⊢ A ∈ No ∧ x ∈ On s → A ∈ L ⁡ x → A ≤ s x
28 20 27 sylbid ⊢ A ∈ No ∧ x ∈ On s → A ∈ L ⁡ x ∪ R ⁡ x → A ≤ s x
29 13 28 biimtrrid ⊢ A ∈ No ∧ x ∈ On s → A ∈ Old ⁡ bday ⁡ x → A ≤ s x
30 newbday ⊢ bday ⁡ x ∈ On ∧ A ∈ No → A ∈ N ⁡ bday ⁡ x ↔ bday ⁡ A = bday ⁡ x
31 1 30 mpan ⊢ A ∈ No → A ∈ N ⁡ bday ⁡ x ↔ bday ⁡ A = bday ⁡ x
32 31 adantr ⊢ A ∈ No ∧ x ∈ On s → A ∈ N ⁡ bday ⁡ x ↔ bday ⁡ A = bday ⁡ x
33 leftssold ⊢ L ⁡ A ⊆ Old ⁡ bday ⁡ A
34 fveq2 ⊢ bday ⁡ A = bday ⁡ x → Old ⁡ bday ⁡ A = Old ⁡ bday ⁡ x
35 34 adantl ⊢ A ∈ No ∧ x ∈ On s ∧ bday ⁡ A = bday ⁡ x → Old ⁡ bday ⁡ A = Old ⁡ bday ⁡ x
36 onsleft ⊢ x ∈ On s → Old ⁡ bday ⁡ x = L ⁡ x
37 36 ad2antlr ⊢ A ∈ No ∧ x ∈ On s ∧ bday ⁡ A = bday ⁡ x → Old ⁡ bday ⁡ x = L ⁡ x
38 35 37 eqtr2d ⊢ A ∈ No ∧ x ∈ On s ∧ bday ⁡ A = bday ⁡ x → L ⁡ x = Old ⁡ bday ⁡ A
39 33 38 sseqtrrid ⊢ A ∈ No ∧ x ∈ On s ∧ bday ⁡ A = bday ⁡ x → L ⁡ A ⊆ L ⁡ x
40 slelss ⊢ A ∈ No ∧ x ∈ No ∧ bday ⁡ A = bday ⁡ x → A ≤ s x ↔ L ⁡ A ⊆ L ⁡ x
41 22 40 syl3an2 ⊢ A ∈ No ∧ x ∈ On s ∧ bday ⁡ A = bday ⁡ x → A ≤ s x ↔ L ⁡ A ⊆ L ⁡ x
42 41 3expa ⊢ A ∈ No ∧ x ∈ On s ∧ bday ⁡ A = bday ⁡ x → A ≤ s x ↔ L ⁡ A ⊆ L ⁡ x
43 39 42 mpbird ⊢ A ∈ No ∧ x ∈ On s ∧ bday ⁡ A = bday ⁡ x → A ≤ s x
44 43 ex ⊢ A ∈ No ∧ x ∈ On s → bday ⁡ A = bday ⁡ x → A ≤ s x
45 32 44 sylbid ⊢ A ∈ No ∧ x ∈ On s → A ∈ N ⁡ bday ⁡ x → A ≤ s x
46 29 45 jaod ⊢ A ∈ No ∧ x ∈ On s → A ∈ Old ⁡ bday ⁡ x ∨ A ∈ N ⁡ bday ⁡ x → A ≤ s x
47 11 46 biimtrid ⊢ A ∈ No ∧ x ∈ On s → A ∈ M ⁡ bday ⁡ x → A ≤ s x
48 madebday ⊢ bday ⁡ x ∈ On ∧ A ∈ No → A ∈ M ⁡ bday ⁡ x ↔ bday ⁡ A ⊆ bday ⁡ x
49 1 48 mpan ⊢ A ∈ No → A ∈ M ⁡ bday ⁡ x ↔ bday ⁡ A ⊆ bday ⁡ x
50 49 adantr ⊢ A ∈ No ∧ x ∈ On s → A ∈ M ⁡ bday ⁡ x ↔ bday ⁡ A ⊆ bday ⁡ x
51 slenlt ⊢ A ∈ No ∧ x ∈ No → A ≤ s x ↔ ¬ x < s A
52 22 51 sylan2 ⊢ A ∈ No ∧ x ∈ On s → A ≤ s x ↔ ¬ x < s A
53 47 50 52 3imtr3d ⊢ A ∈ No ∧ x ∈ On s → bday ⁡ A ⊆ bday ⁡ x → ¬ x < s A
54 53 con2d ⊢ A ∈ No ∧ x ∈ On s → x < s A → ¬ bday ⁡ A ⊆ bday ⁡ x
55 54 3impia ⊢ A ∈ No ∧ x ∈ On s ∧ x < s A → ¬ bday ⁡ A ⊆ bday ⁡ x
56 7 55 olcnd ⊢ A ∈ No ∧ x ∈ On s ∧ x < s A → bday ⁡ x ∈ bday ⁡ A
57 22 3ad2ant2 ⊢ A ∈ No ∧ x ∈ On s ∧ x < s A → x ∈ No
58 oldbday ⊢ bday ⁡ A ∈ On ∧ x ∈ No → x ∈ Old ⁡ bday ⁡ A ↔ bday ⁡ x ∈ bday ⁡ A
59 3 57 58 sylancr ⊢ A ∈ No ∧ x ∈ On s ∧ x < s A → x ∈ Old ⁡ bday ⁡ A ↔ bday ⁡ x ∈ bday ⁡ A
60 56 59 mpbird ⊢ A ∈ No ∧ x ∈ On s ∧ x < s A → x ∈ Old ⁡ bday ⁡ A
61 60 rabssdv ⊢ A ∈ No → x ∈ On s | x < s A ⊆ Old ⁡ bday ⁡ A