Theorem n0sbday

Description: A non-negative surreal integer has a finite birthday. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Assertion	n0sbday	⊢ ( 𝐴 ∈ ℕ0s → ( bday ‘ 𝐴 ) ∈ ω )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑚 = 0s → ( bday ‘ 𝑚 ) = ( bday ‘ 0s ) )
2	1	eleq1d	⊢ ( 𝑚 = 0s → ( ( bday ‘ 𝑚 ) ∈ ω ↔ ( bday ‘ 0s ) ∈ ω ) )
3		fveq2	⊢ ( 𝑚 = 𝑛 → ( bday ‘ 𝑚 ) = ( bday ‘ 𝑛 ) )
4	3	eleq1d	⊢ ( 𝑚 = 𝑛 → ( ( bday ‘ 𝑚 ) ∈ ω ↔ ( bday ‘ 𝑛 ) ∈ ω ) )
5		fveq2	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( bday ‘ 𝑚 ) = ( bday ‘ ( 𝑛 +s 1s ) ) )
6	5	eleq1d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( bday ‘ 𝑚 ) ∈ ω ↔ ( bday ‘ ( 𝑛 +s 1s ) ) ∈ ω ) )
7		fveq2	⊢ ( 𝑚 = 𝐴 → ( bday ‘ 𝑚 ) = ( bday ‘ 𝐴 ) )
8	7	eleq1d	⊢ ( 𝑚 = 𝐴 → ( ( bday ‘ 𝑚 ) ∈ ω ↔ ( bday ‘ 𝐴 ) ∈ ω ) )
9		bday0s	⊢ ( bday ‘ 0s ) = ∅
10		peano1	⊢ ∅ ∈ ω
11	9 10	eqeltri	⊢ ( bday ‘ 0s ) ∈ ω
12		peano2n0s	⊢ ( 𝑛 ∈ ℕ0s → ( 𝑛 +s 1s ) ∈ ℕ0s )
13		n0scut	⊢ ( ( 𝑛 +s 1s ) ∈ ℕ0s → ( 𝑛 +s 1s ) = ( { ( ( 𝑛 +s 1s ) -s 1s ) } |s ∅ ) )
14	12 13	syl	⊢ ( 𝑛 ∈ ℕ0s → ( 𝑛 +s 1s ) = ( { ( ( 𝑛 +s 1s ) -s 1s ) } |s ∅ ) )
15		n0sno	⊢ ( 𝑛 ∈ ℕ0s → 𝑛 ∈ No )
16		1sno	⊢ 1s ∈ No
17		pncans	⊢ ( ( 𝑛 ∈ No ∧ 1s ∈ No ) → ( ( 𝑛 +s 1s ) -s 1s ) = 𝑛 )
18	15 16 17	sylancl	⊢ ( 𝑛 ∈ ℕ0s → ( ( 𝑛 +s 1s ) -s 1s ) = 𝑛 )
19	18	sneqd	⊢ ( 𝑛 ∈ ℕ0s → { ( ( 𝑛 +s 1s ) -s 1s ) } = { 𝑛 } )
20	19	oveq1d	⊢ ( 𝑛 ∈ ℕ0s → ( { ( ( 𝑛 +s 1s ) -s 1s ) } |s ∅ ) = ( { 𝑛 } |s ∅ ) )
21	14 20	eqtrd	⊢ ( 𝑛 ∈ ℕ0s → ( 𝑛 +s 1s ) = ( { 𝑛 } |s ∅ ) )
22	21	fveq2d	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ ( 𝑛 +s 1s ) ) = ( bday ‘ ( { 𝑛 } |s ∅ ) ) )
23		snelpwi	⊢ ( 𝑛 ∈ No → { 𝑛 } ∈ 𝒫 No )
24		nulssgt	⊢ ( { 𝑛 } ∈ 𝒫 No → { 𝑛 } <<s ∅ )
25	15 23 24	3syl	⊢ ( 𝑛 ∈ ℕ0s → { 𝑛 } <<s ∅ )
26		un0	⊢ ( { 𝑛 } ∪ ∅ ) = { 𝑛 }
27	26	imaeq2i	⊢ ( bday “ ( { 𝑛 } ∪ ∅ ) ) = ( bday “ { 𝑛 } )
28		bdayfn	⊢ bday Fn No
29		fnsnfv	⊢ ( ( bday Fn No ∧ 𝑛 ∈ No ) → { ( bday ‘ 𝑛 ) } = ( bday “ { 𝑛 } ) )
30	28 15 29	sylancr	⊢ ( 𝑛 ∈ ℕ0s → { ( bday ‘ 𝑛 ) } = ( bday “ { 𝑛 } ) )
31	27 30	eqtr4id	⊢ ( 𝑛 ∈ ℕ0s → ( bday “ ( { 𝑛 } ∪ ∅ ) ) = { ( bday ‘ 𝑛 ) } )
32		fvex	⊢ ( bday ‘ 𝑛 ) ∈ V
33	32	sucid	⊢ ( bday ‘ 𝑛 ) ∈ suc ( bday ‘ 𝑛 )
34		snssi	⊢ ( ( bday ‘ 𝑛 ) ∈ suc ( bday ‘ 𝑛 ) → { ( bday ‘ 𝑛 ) } ⊆ suc ( bday ‘ 𝑛 ) )
35	33 34	ax-mp	⊢ { ( bday ‘ 𝑛 ) } ⊆ suc ( bday ‘ 𝑛 )
36	31 35	eqsstrdi	⊢ ( 𝑛 ∈ ℕ0s → ( bday “ ( { 𝑛 } ∪ ∅ ) ) ⊆ suc ( bday ‘ 𝑛 ) )
37		bdayelon	⊢ ( bday ‘ 𝑛 ) ∈ On
38	37	onsuci	⊢ suc ( bday ‘ 𝑛 ) ∈ On
39		scutbdaybnd	⊢ ( ( { 𝑛 } <<s ∅ ∧ suc ( bday ‘ 𝑛 ) ∈ On ∧ ( bday “ ( { 𝑛 } ∪ ∅ ) ) ⊆ suc ( bday ‘ 𝑛 ) ) → ( bday ‘ ( { 𝑛 } |s ∅ ) ) ⊆ suc ( bday ‘ 𝑛 ) )
40	38 39	mp3an2	⊢ ( ( { 𝑛 } <<s ∅ ∧ ( bday “ ( { 𝑛 } ∪ ∅ ) ) ⊆ suc ( bday ‘ 𝑛 ) ) → ( bday ‘ ( { 𝑛 } |s ∅ ) ) ⊆ suc ( bday ‘ 𝑛 ) )
41	25 36 40	syl2anc	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ ( { 𝑛 } |s ∅ ) ) ⊆ suc ( bday ‘ 𝑛 ) )
42	22 41	eqsstrd	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ ( 𝑛 +s 1s ) ) ⊆ suc ( bday ‘ 𝑛 ) )
43		bdayelon	⊢ ( bday ‘ ( 𝑛 +s 1s ) ) ∈ On
44		onsssuc	⊢ ( ( ( bday ‘ ( 𝑛 +s 1s ) ) ∈ On ∧ suc ( bday ‘ 𝑛 ) ∈ On ) → ( ( bday ‘ ( 𝑛 +s 1s ) ) ⊆ suc ( bday ‘ 𝑛 ) ↔ ( bday ‘ ( 𝑛 +s 1s ) ) ∈ suc suc ( bday ‘ 𝑛 ) ) )
45	43 38 44	mp2an	⊢ ( ( bday ‘ ( 𝑛 +s 1s ) ) ⊆ suc ( bday ‘ 𝑛 ) ↔ ( bday ‘ ( 𝑛 +s 1s ) ) ∈ suc suc ( bday ‘ 𝑛 ) )
46	42 45	sylib	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ ( 𝑛 +s 1s ) ) ∈ suc suc ( bday ‘ 𝑛 ) )
47		peano2	⊢ ( ( bday ‘ 𝑛 ) ∈ ω → suc ( bday ‘ 𝑛 ) ∈ ω )
48		peano2	⊢ ( suc ( bday ‘ 𝑛 ) ∈ ω → suc suc ( bday ‘ 𝑛 ) ∈ ω )
49	47 48	syl	⊢ ( ( bday ‘ 𝑛 ) ∈ ω → suc suc ( bday ‘ 𝑛 ) ∈ ω )
50		elnn	⊢ ( ( ( bday ‘ ( 𝑛 +s 1s ) ) ∈ suc suc ( bday ‘ 𝑛 ) ∧ suc suc ( bday ‘ 𝑛 ) ∈ ω ) → ( bday ‘ ( 𝑛 +s 1s ) ) ∈ ω )
51	46 49 50	syl2an	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( bday ‘ 𝑛 ) ∈ ω ) → ( bday ‘ ( 𝑛 +s 1s ) ) ∈ ω )
52	51	ex	⊢ ( 𝑛 ∈ ℕ0s → ( ( bday ‘ 𝑛 ) ∈ ω → ( bday ‘ ( 𝑛 +s 1s ) ) ∈ ω ) )
53	2 4 6 8 11 52	n0sind	⊢ ( 𝐴 ∈ ℕ0s → ( bday ‘ 𝐴 ) ∈ ω )