Theorem ltonold 28412

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 27903	. . . . . . 7 ⊢ ( bday ‘𝑥) ∈ On
2	1	onordi 6463	. . . . . 6 ⊢ Ord ( bday ‘𝑥)
3		bdayon 27903	. . . . . . 7 ⊢ ( bday ‘𝐴) ∈ On
4	3	onordi 6463	. . . . . 6 ⊢ Ord ( bday ‘𝐴)
5		ordtri2or 6450	. . . . . 6 ⊢ ((Ord ( bday ‘𝑥) ∧ Ord ( bday ‘𝐴)) → (( bday ‘𝑥) ∈ ( bday ‘𝐴) ∨ ( bday ‘𝐴) ⊆ ( bday ‘𝑥)))
6	2, 4, 5	mp2an 704	. . . . 5 ⊢ (( bday ‘𝑥) ∈ ( bday ‘𝐴) ∨ ( bday ‘𝐴) ⊆ ( bday ‘𝑥))
7	6	a1i 11	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴) → (( bday ‘𝑥) ∈ ( bday ‘𝐴) ∨ ( bday ‘𝐴) ⊆ ( bday ‘𝑥)))
8		madeun 28035	. . . . . . . . . 10 ⊢ ( M ‘( bday ‘𝑥)) = (( O ‘( bday ‘𝑥)) ∪ ( N ‘( bday ‘𝑥)))
9	8	eleq2i 2857	. . . . . . . . 9 ⊢ (𝐴 ∈ ( M ‘( bday ‘𝑥)) ↔ 𝐴 ∈ (( O ‘( bday ‘𝑥)) ∪ ( N ‘( bday ‘𝑥))))
10		elun 4109	. . . . . . . . 9 ⊢ (𝐴 ∈ (( O ‘( bday ‘𝑥)) ∪ ( N ‘( bday ‘𝑥))) ↔ (𝐴 ∈ ( O ‘( bday ‘𝑥)) ∨ 𝐴 ∈ ( N ‘( bday ‘𝑥))))
11	9, 10	bitri 278	. . . . . . . 8 ⊢ (𝐴 ∈ ( M ‘( bday ‘𝑥)) ↔ (𝐴 ∈ ( O ‘( bday ‘𝑥)) ∨ 𝐴 ∈ ( N ‘( bday ‘𝑥))))
12		lrold 28048	. . . . . . . . . . 11 ⊢ (( L ‘𝑥) ∪ ( R ‘𝑥)) = ( O ‘( bday ‘𝑥))
13	12	eleq2i 2857	. . . . . . . . . 10 ⊢ (𝐴 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)) ↔ 𝐴 ∈ ( O ‘( bday ‘𝑥)))
14		elons 28404	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Ons ↔ (𝑥 ∈ No ∧ ( R ‘𝑥) = ∅))
15	14	simprbi 502	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Ons → ( R ‘𝑥) = ∅)
16	15	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → ( R ‘𝑥) = ∅)
17	16	uneq2d 4124	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (( L ‘𝑥) ∪ ( R ‘𝑥)) = (( L ‘𝑥) ∪ ∅))
18		un0 4351	. . . . . . . . . . . . 13 ⊢ (( L ‘𝑥) ∪ ∅) = ( L ‘𝑥)
19	17, 18	eqtrdi 2816	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (( L ‘𝑥) ∪ ( R ‘𝑥)) = ( L ‘𝑥))
20	19	eleq2d 2851	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)) ↔ 𝐴 ∈ ( L ‘𝑥)))
21		simpll 778	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ 𝐴 ∈ ( L ‘𝑥)) → 𝐴 ∈ No )
22		onno 28406	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ Ons → 𝑥 ∈ No )
23	22	ad2antlr 739	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ 𝐴 ∈ ( L ‘𝑥)) → 𝑥 ∈ No )
24		leftlt 28004	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ( L ‘𝑥) → 𝐴 <s 𝑥)
25	24	adantl 486	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ 𝐴 ∈ ( L ‘𝑥)) → 𝐴 <s 𝑥)
26	21, 23, 25	ltlesd 27895	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ 𝐴 ∈ ( L ‘𝑥)) → 𝐴 ≤s 𝑥)
27	26	ex 417	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ ( L ‘𝑥) → 𝐴 ≤s 𝑥))
28	20, 27	sylbid 243	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)) → 𝐴 ≤s 𝑥))
29	13, 28	biimtrrid 246	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ ( O ‘( bday ‘𝑥)) → 𝐴 ≤s 𝑥))
30		newbday 28053	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑥) ∈ On ∧ 𝐴 ∈ No ) → (𝐴 ∈ ( N ‘( bday ‘𝑥)) ↔ ( bday ‘𝐴) = ( bday ‘𝑥)))
31	1, 30	mpan 702	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → (𝐴 ∈ ( N ‘( bday ‘𝑥)) ↔ ( bday ‘𝐴) = ( bday ‘𝑥)))
32	31	adantr 485	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ ( N ‘( bday ‘𝑥)) ↔ ( bday ‘𝐴) = ( bday ‘𝑥)))
33		leftssold 28022	. . . . . . . . . . . . 13 ⊢ ( L ‘𝐴) ⊆ ( O ‘( bday ‘𝐴))
34		fveq2 6871	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝐴) = ( bday ‘𝑥) → ( O ‘( bday ‘𝐴)) = ( O ‘( bday ‘𝑥)))
35	34	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → ( O ‘( bday ‘𝐴)) = ( O ‘( bday ‘𝑥)))
36		onleft 28411	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Ons → ( O ‘( bday ‘𝑥)) = ( L ‘𝑥))
37	36	ad2antlr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → ( O ‘( bday ‘𝑥)) = ( L ‘𝑥))
38	35, 37	eqtr2d 2801	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → ( L ‘𝑥) = ( O ‘( bday ‘𝐴)))
39	33, 38	sseqtrrid 3982	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → ( L ‘𝐴) ⊆ ( L ‘𝑥))
40		leslss 28060	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ No ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → (𝐴 ≤s 𝑥 ↔ ( L ‘𝐴) ⊆ ( L ‘𝑥)))
41	22, 40	syl3an2 1180	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → (𝐴 ≤s 𝑥 ↔ ( L ‘𝐴) ⊆ ( L ‘𝑥)))
42	41	3expa 1134	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → (𝐴 ≤s 𝑥 ↔ ( L ‘𝐴) ⊆ ( L ‘𝑥)))
43	39, 42	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ No ∧ 𝑥 ∈ Ons) ∧ ( bday ‘𝐴) = ( bday ‘𝑥)) → 𝐴 ≤s 𝑥)
44	43	ex 417	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (( bday ‘𝐴) = ( bday ‘𝑥) → 𝐴 ≤s 𝑥))
45	32, 44	sylbid 243	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ ( N ‘( bday ‘𝑥)) → 𝐴 ≤s 𝑥))
46	29, 45	jaod 872	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → ((𝐴 ∈ ( O ‘( bday ‘𝑥)) ∨ 𝐴 ∈ ( N ‘( bday ‘𝑥))) → 𝐴 ≤s 𝑥))
47	11, 46	biimtrid 245	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ ( M ‘( bday ‘𝑥)) → 𝐴 ≤s 𝑥))
48		madebday 28051	. . . . . . . . 9 ⊢ ((( bday ‘𝑥) ∈ On ∧ 𝐴 ∈ No ) → (𝐴 ∈ ( M ‘( bday ‘𝑥)) ↔ ( bday ‘𝐴) ⊆ ( bday ‘𝑥)))
49	1, 48	mpan 702	. . . . . . . 8 ⊢ (𝐴 ∈ No → (𝐴 ∈ ( M ‘( bday ‘𝑥)) ↔ ( bday ‘𝐴) ⊆ ( bday ‘𝑥)))
50	49	adantr 485	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ∈ ( M ‘( bday ‘𝑥)) ↔ ( bday ‘𝐴) ⊆ ( bday ‘𝑥)))
51		lenlts 27874	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ No ) → (𝐴 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝐴))
52	22, 51	sylan2 604	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝐴 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝐴))
53	47, 50, 52	3imtr3d 296	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (( bday ‘𝐴) ⊆ ( bday ‘𝑥) → ¬ 𝑥 <s 𝐴))
54	53	con2d 135	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons) → (𝑥 <s 𝐴 → ¬ ( bday ‘𝐴) ⊆ ( bday ‘𝑥)))
55	54	3impia 1133	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴) → ¬ ( bday ‘𝐴) ⊆ ( bday ‘𝑥))
56	7, 55	olcnd 890	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴) → ( bday ‘𝑥) ∈ ( bday ‘𝐴))
57	22	3ad2ant2 1150	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴) → 𝑥 ∈ No )
58		oldbday 28052	. . . 4 ⊢ ((( bday ‘𝐴) ∈ On ∧ 𝑥 ∈ No ) → (𝑥 ∈ ( O ‘( bday ‘𝐴)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝐴)))
59	3, 57, 58	sylancr 598	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴) → (𝑥 ∈ ( O ‘( bday ‘𝐴)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝐴)))
60	56, 59	mpbird 260	. 2 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴) → 𝑥 ∈ ( O ‘( bday ‘𝐴)))
61	60	rabssdv 4030	1 ⊢ (𝐴 ∈ No → {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} ⊆ ( O ‘( bday ‘𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  {crab 3417   ∪ cun 3905   ⊆ wss 3907  ∅c0 4288   class class class wbr 5105  Ord word 6349  Oncon0 6350  ‘cfv 6525   No csur 27762   <s clts 27763   bday cbday 27764   ≤s cles 27866   M cmade 27973   O cold 27974   N cnew 27975   L cleft 27976   R cright 27977  On_scons 28402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4869  df-int 4909  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-1o 8441  df-2o 8442  df-no 27765  df-lts 27766  df-bday 27767  df-les 27867  df-slts 27909  df-cuts 27911  df-made 27978  df-old 27979  df-new 27980  df-left 27981  df-right 27982  df-ons 28403

This theorem is referenced by:  ltonsex  28413  onsfi  28507