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		n0scut2	⊢ ( 𝑛 ∈ ℕ0s → ( 𝑛 +s 1s ) = ( { 𝑛 } |s ∅ ) )
13	12	fveq2d	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ ( 𝑛 +s 1s ) ) = ( bday ‘ ( { 𝑛 } |s ∅ ) ) )
14		n0sno	⊢ ( 𝑛 ∈ ℕ0s → 𝑛 ∈ No )
15		snelpwi	⊢ ( 𝑛 ∈ No → { 𝑛 } ∈ 𝒫 No )
16		nulssgt	⊢ ( { 𝑛 } ∈ 𝒫 No → { 𝑛 } <<s ∅ )
17	14 15 16	3syl	⊢ ( 𝑛 ∈ ℕ0s → { 𝑛 } <<s ∅ )
18		un0	⊢ ( { 𝑛 } ∪ ∅ ) = { 𝑛 }
19	18	imaeq2i	⊢ ( bday “ ( { 𝑛 } ∪ ∅ ) ) = ( bday “ { 𝑛 } )
20		bdayfn	⊢ bday Fn No
21		fnsnfv	⊢ ( ( bday Fn No ∧ 𝑛 ∈ No ) → { ( bday ‘ 𝑛 ) } = ( bday “ { 𝑛 } ) )
22	20 14 21	sylancr	⊢ ( 𝑛 ∈ ℕ0s → { ( bday ‘ 𝑛 ) } = ( bday “ { 𝑛 } ) )
23	19 22	eqtr4id	⊢ ( 𝑛 ∈ ℕ0s → ( bday “ ( { 𝑛 } ∪ ∅ ) ) = { ( bday ‘ 𝑛 ) } )
24		fvex	⊢ ( bday ‘ 𝑛 ) ∈ V
25	24	sucid	⊢ ( bday ‘ 𝑛 ) ∈ suc ( bday ‘ 𝑛 )
26		snssi	⊢ ( ( bday ‘ 𝑛 ) ∈ suc ( bday ‘ 𝑛 ) → { ( bday ‘ 𝑛 ) } ⊆ suc ( bday ‘ 𝑛 ) )
27	25 26	ax-mp	⊢ { ( bday ‘ 𝑛 ) } ⊆ suc ( bday ‘ 𝑛 )
28	23 27	eqsstrdi	⊢ ( 𝑛 ∈ ℕ0s → ( bday “ ( { 𝑛 } ∪ ∅ ) ) ⊆ suc ( bday ‘ 𝑛 ) )
29		bdayelon	⊢ ( bday ‘ 𝑛 ) ∈ On
30	29	onsuci	⊢ suc ( bday ‘ 𝑛 ) ∈ On
31		scutbdaybnd	⊢ ( ( { 𝑛 } <<s ∅ ∧ suc ( bday ‘ 𝑛 ) ∈ On ∧ ( bday “ ( { 𝑛 } ∪ ∅ ) ) ⊆ suc ( bday ‘ 𝑛 ) ) → ( bday ‘ ( { 𝑛 } |s ∅ ) ) ⊆ suc ( bday ‘ 𝑛 ) )
32	30 31	mp3an2	⊢ ( ( { 𝑛 } <<s ∅ ∧ ( bday “ ( { 𝑛 } ∪ ∅ ) ) ⊆ suc ( bday ‘ 𝑛 ) ) → ( bday ‘ ( { 𝑛 } |s ∅ ) ) ⊆ suc ( bday ‘ 𝑛 ) )
33	17 28 32	syl2anc	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ ( { 𝑛 } |s ∅ ) ) ⊆ suc ( bday ‘ 𝑛 ) )
34	13 33	eqsstrd	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ ( 𝑛 +s 1s ) ) ⊆ suc ( bday ‘ 𝑛 ) )
35		bdayelon	⊢ ( bday ‘ ( 𝑛 +s 1s ) ) ∈ On
36		onsssuc	⊢ ( ( ( bday ‘ ( 𝑛 +s 1s ) ) ∈ On ∧ suc ( bday ‘ 𝑛 ) ∈ On ) → ( ( bday ‘ ( 𝑛 +s 1s ) ) ⊆ suc ( bday ‘ 𝑛 ) ↔ ( bday ‘ ( 𝑛 +s 1s ) ) ∈ suc suc ( bday ‘ 𝑛 ) ) )
37	35 30 36	mp2an	⊢ ( ( bday ‘ ( 𝑛 +s 1s ) ) ⊆ suc ( bday ‘ 𝑛 ) ↔ ( bday ‘ ( 𝑛 +s 1s ) ) ∈ suc suc ( bday ‘ 𝑛 ) )
38	34 37	sylib	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ ( 𝑛 +s 1s ) ) ∈ suc suc ( bday ‘ 𝑛 ) )
39		peano2	⊢ ( ( bday ‘ 𝑛 ) ∈ ω → suc ( bday ‘ 𝑛 ) ∈ ω )
40		peano2	⊢ ( suc ( bday ‘ 𝑛 ) ∈ ω → suc suc ( bday ‘ 𝑛 ) ∈ ω )
41	39 40	syl	⊢ ( ( bday ‘ 𝑛 ) ∈ ω → suc suc ( bday ‘ 𝑛 ) ∈ ω )
42		elnn	⊢ ( ( ( bday ‘ ( 𝑛 +s 1s ) ) ∈ suc suc ( bday ‘ 𝑛 ) ∧ suc suc ( bday ‘ 𝑛 ) ∈ ω ) → ( bday ‘ ( 𝑛 +s 1s ) ) ∈ ω )
43	38 41 42	syl2an	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( bday ‘ 𝑛 ) ∈ ω ) → ( bday ‘ ( 𝑛 +s 1s ) ) ∈ ω )
44	43	ex	⊢ ( 𝑛 ∈ ℕ0s → ( ( bday ‘ 𝑛 ) ∈ ω → ( bday ‘ ( 𝑛 +s 1s ) ) ∈ ω ) )
45	2 4 6 8 11 44	n0sind	⊢ ( 𝐴 ∈ ℕ0s → ( bday ‘ 𝐴 ) ∈ ω )