Theorem ltonold 28331

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.)

Assertion

Ref	Expression
ltonold	⊢ (𝐴 ∈ No → {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} ⊆ ( O ‘( bday ‘𝐴)))

Distinct variable group:   𝑥,𝐴

Proof of Theorem ltonold

Step	Hyp	Ref	Expression
1		bdayon 27822	. . . . . . 7 ⊢ ( bday ‘𝑥) ∈ On
2	1	onordi 6455	. . . . . 6 ⊢ Ord ( bday ‘𝑥)
3		bdayon 27822	. . . . . . 7 ⊢ ( bday ‘𝐴) ∈ On
4	3	onordi 6455	. . . . . 6 ⊢ Ord ( bday ‘𝐴)
5		ordtri2or 6442	. . . . . 6 ⊢ ((Ord ( bday ‘𝑥) ∧ Ord ( bday ‘𝐴)) → (( bday ‘𝑥) ∈ ( bday ‘𝐴) ∨ ( bday ‘𝐴) ⊆ ( bday ‘𝑥)))
6	2, 4, 5	mp2an 702	. . . . 5 ⊢ (( bday ‘𝑥) ∈ ( bday ‘𝐴) ∨ ( bday ‘𝐴) ⊆ ( bday ‘𝑥))
7	6	a1i 11	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴) → (( bday ‘𝑥) ∈ ( bday ‘𝐴) ∨ ( bday ‘𝐴) ⊆ ( bday ‘𝑥)))
8		madeun 27954	. . . . . . . . . 10 ⊢ ( M ‘( bday ‘𝑥)) = (( O ‘( bday ‘𝑥)) ∪ ( N ‘( bday ‘𝑥)))
9	8	eleq2i 2853	. . . . . . . . 9 ⊢ (𝐴 ∈ ( M ‘( bday ‘𝑥)) ↔ 𝐴 ∈ (( O ‘( bday ‘𝑥)) ∪ ( N ‘( bday ‘𝑥))))
10		elun 4106	. . . . . . . . 9 ⊢ (𝐴 ∈ (( O ‘( bday ‘𝑥)) ∪ ( N ‘( bday ‘𝑥))) ↔ (𝐴 ∈ ( O ‘( bday ‘𝑥)) ∨ 𝐴 ∈ ( N ‘( bday ‘𝑥))))
11	9, 10	bitri 277	. . . . . . . 8 ⊢ (𝐴 ∈ ( M ‘( bday ‘𝑥)) ↔ (𝐴 ∈ ( O ‘( bday ‘𝑥)) ∨ 𝐴 ∈ ( N ‘( bday ‘𝑥))))
12		lrold 27967	. . . . . . . . . . 11 ⊢ (( L ‘𝑥) ∪ ( R ‘𝑥)) = ( O ‘( bday ‘𝑥))
13	12	eleq2i 2853	. . . . . . . . . 10 ⊢ (𝐴 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)) ↔ 𝐴 ∈ ( O ‘( bday ‘𝑥)))
14		elons 28323	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Ons ↔ (𝑥 ∈ No ∧ ( R ‘𝑥) = ∅))
15	14	simprbi 501	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Ons → ( R ‘𝑥) = ∅)
16	15	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → ( R ‘𝑥) = ∅)
17	16	uneq2d 4121	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (( L ‘𝑥) ∪ ( R ‘𝑥)) = (( L ‘𝑥) ∪ ∅))
18		un0 4347	. . . . . . . . . . . . 13 ⊢ (( L ‘𝑥) ∪ ∅) = ( L ‘𝑥)
19	17, 18	eqtrdi 2812	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (( L ‘𝑥) ∪ ( R ‘𝑥)) = ( L ‘𝑥))
20	19	eleq2d 2847	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)) ↔ 𝐴 ∈ ( L ‘𝑥)))
21		simpll 776	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ 𝐴 ∈ ( L ‘𝑥)) → 𝐴 ∈ No )
22		onno 28325	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ Ons → 𝑥 ∈ No )
23	22	ad2antlr 737	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ 𝐴 ∈ ( L ‘𝑥)) → 𝑥 ∈ No )
24		leftlt 27923	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ( L ‘𝑥) → 𝐴 <s 𝑥)
25	24	adantl 485	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ 𝐴 ∈ ( L ‘𝑥)) → 𝐴 <s 𝑥)
26	21, 23, 25	ltlesd 27814	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ 𝐴 ∈ ( L ‘𝑥)) → 𝐴 ≤s 𝑥)
27	26	ex 416	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ ( L ‘𝑥) → 𝐴 ≤s 𝑥))
28	20, 27	sylbid 242	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)) → 𝐴 ≤s 𝑥))
29	13, 28	biimtrrid 245	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ ( O ‘( bday ‘𝑥)) → 𝐴 ≤s 𝑥))
30		newbday 27972	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑥) ∈ On ∧ 𝐴 ∈ No ) → (𝐴 ∈ ( N ‘( bday ‘𝑥)) ↔ ( bday ‘𝐴) = ( bday ‘𝑥)))
31	1, 30	mpan 700	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → (𝐴 ∈ ( N ‘( bday ‘𝑥)) ↔ ( bday ‘𝐴) = ( bday ‘𝑥)))
32	31	adantr 484	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ ( N ‘( bday ‘𝑥)) ↔ ( bday ‘𝐴) = ( bday ‘𝑥)))
33		leftssold 27941	. . . . . . . . . . . . 13 ⊢ ( L ‘𝐴) ⊆ ( O ‘( bday ‘𝐴))
34		fveq2 6863	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝐴) = ( bday ‘𝑥) → ( O ‘( bday ‘𝐴)) = ( O ‘( bday ‘𝑥)))
35	34	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → ( O ‘( bday ‘𝐴)) = ( O ‘( bday ‘𝑥)))
36		onleft 28330	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Ons → ( O ‘( bday ‘𝑥)) = ( L ‘𝑥))
37	36	ad2antlr 737	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → ( O ‘( bday ‘𝑥)) = ( L ‘𝑥))
38	35, 37	eqtr2d 2797	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → ( L ‘𝑥) = ( O ‘( bday ‘𝐴)))
39	33, 38	sseqtrrid 3979	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → ( L ‘𝐴) ⊆ ( L ‘𝑥))
40		leslss 27979	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ No ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → (𝐴 ≤s 𝑥 ↔ ( L ‘𝐴) ⊆ ( L ‘𝑥)))
41	22, 40	syl3an2 1176	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → (𝐴 ≤s 𝑥 ↔ ( L ‘𝐴) ⊆ ( L ‘𝑥)))
42	41	3expa 1130	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → (𝐴 ≤s 𝑥 ↔ ( L ‘𝐴) ⊆ ( L ‘𝑥)))
43	39, 42	mpbird 259	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → 𝐴 ≤s 𝑥)
44	43	ex 416	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (( bday ‘𝐴) = ( bday ‘𝑥) → 𝐴 ≤s 𝑥))
45	32, 44	sylbid 242	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ ( N ‘( bday ‘𝑥)) → 𝐴 ≤s 𝑥))
46	29, 45	jaod 870	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → ((𝐴 ∈ ( O ‘( bday ‘𝑥)) ∨ 𝐴 ∈ ( N ‘( bday ‘𝑥))) → 𝐴 ≤s 𝑥))
47	11, 46	biimtrid 244	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ ( M ‘( bday ‘𝑥)) → 𝐴 ≤s 𝑥))
48		madebday 27970	. . . . . . . . 9 ⊢ ((( bday ‘𝑥) ∈ On ∧ 𝐴 ∈ No ) → (𝐴 ∈ ( M ‘( bday ‘𝑥)) ↔ ( bday ‘𝐴) ⊆ ( bday ‘𝑥)))
49	1, 48	mpan 700	. . . . . . . 8 ⊢ (𝐴 ∈ No → (𝐴 ∈ ( M ‘( bday ‘𝑥)) ↔ ( bday ‘𝐴) ⊆ ( bday ‘𝑥)))
50	49	adantr 484	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ ( M ‘( bday ‘𝑥)) ↔ ( bday ‘𝐴) ⊆ ( bday ‘𝑥)))
51		lenlts 27793	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ No ) → (𝐴 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝐴))
52	22, 51	sylan2 602	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝐴))
53	47, 50, 52	3imtr3d 295	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (( bday ‘𝐴) ⊆ ( bday ‘𝑥) → ¬ 𝑥 <s 𝐴))
54	53	con2d 134	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝑥 <s 𝐴 → ¬ ( bday ‘𝐴) ⊆ ( bday ‘𝑥)))
55	54	3impia 1129	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴) → ¬ ( bday ‘𝐴) ⊆ ( bday ‘𝑥))
56	7, 55	olcnd 888	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴) → ( bday ‘𝑥) ∈ ( bday ‘𝐴))
57	22	3ad2ant2 1146	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴) → 𝑥 ∈ No )
58		oldbday 27971	. . . 4 ⊢ ((( bday ‘𝐴) ∈ On ∧ 𝑥 ∈ No ) → (𝑥 ∈ ( O ‘( bday ‘𝐴)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝐴)))
59	3, 57, 58	sylancr 596	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴) → (𝑥 ∈ ( O ‘( bday ‘𝐴)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝐴)))
60	56, 59	mpbird 259	. 2 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴) → 𝑥 ∈ ( O ‘( bday ‘𝐴)))
61	60	rabssdv 4027	1 ⊢ (𝐴 ∈ No → {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} ⊆ ( O ‘( bday ‘𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  {crab 3413   ∪ cun 3902   ⊆ wss 3904  ∅c0 4285   class class class wbr 5099  Ord word 6341  Oncon0 6342  ‘cfv 6517   No csur 27681   <s clts 27682   bday cbday 27683   ≤s cles 27785   M cmade 27892   O cold 27893   N cnew 27894   L cleft 27895   R cright 27896  On_scons 28321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-tp 4586  df-op 4588  df-uni 4865  df-int 4905  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-riota 7349  df-ov 7395  df-oprab 7396  df-mpo 7397  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-1o 8432  df-2o 8433  df-no 27684  df-lts 27685  df-bday 27686  df-les 27786  df-slts 27828  df-cuts 27830  df-made 27897  df-old 27898  df-new 27899  df-left 27900  df-right 27901  df-ons 28322

This theorem is referenced by:  ltonsex  28332  onsfi  28426