n0sbday

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

		Ref	Expression
	Assertion	n0sbday	$⊢ A \in ℕ_{0s} \to bday (A) \in ω$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ m = 0_{s} \to bday (m) = bday (0_{s})$
2	1	eleq1d	$⊢ m = 0_{s} \to (bday (m) \in ω \leftrightarrow bday (0_{s}) \in ω)$
3		fveq2	$⊢ m = n \to bday (m) = bday (n)$
4	3	eleq1d	$⊢ m = n \to (bday (m) \in ω \leftrightarrow bday (n) \in ω)$
5		fveq2	$⊢ m = n +_{s} 1_{s} \to bday (m) = bday (n +_{s} 1_{s})$
6	5	eleq1d	$⊢ m = n +_{s} 1_{s} \to (bday (m) \in ω \leftrightarrow bday (n +_{s} 1_{s}) \in ω)$
7		fveq2	$⊢ m = A \to bday (m) = bday (A)$
8	7	eleq1d	$⊢ m = A \to (bday (m) \in ω \leftrightarrow bday (A) \in ω)$
9		bday0s	$⊢ bday (0_{s}) = \emptyset$
10		peano1	$⊢ \emptyset \in ω$
11	9 10	eqeltri	$⊢ bday (0_{s}) \in ω$
12		n0scut2	$⊢ n \in ℕ_{0s} \to n +_{s} 1_{s} = \{n\} \|_{s} \emptyset$
13	12	fveq2d	$⊢ n \in ℕ_{0s} \to bday (n +_{s} 1_{s}) = bday (\{n\} \|_{s} \emptyset)$
14		n0sno	$⊢ n \in ℕ_{0s} \to n \in No$
15		snelpwi	$⊢ n \in No \to \{n\} \in 𝒫 No$
16		nulssgt	$⊢ \{n\} \in 𝒫 No \to \{n\} ≪_{s} \emptyset$
17	14 15 16	3syl	$⊢ n \in ℕ_{0s} \to \{n\} ≪_{s} \emptyset$
18		un0	$⊢ \{n\} \cup \emptyset = \{n\}$
19	18	imaeq2i	$⊢ bday [\{n\} \cup \emptyset] = bday [\{n\}]$
20		bdayfn	$⊢ bday Fn No$
21		fnsnfv	$⊢ (bday Fn No \land n \in No) \to \{bday (n)\} = bday [\{n\}]$
22	20 14 21	sylancr	$⊢ n \in ℕ_{0s} \to \{bday (n)\} = bday [\{n\}]$
23	19 22	eqtr4id	$⊢ n \in ℕ_{0s} \to bday [\{n\} \cup \emptyset] = \{bday (n)\}$
24		fvex	$⊢ bday (n) \in V$
25	24	sucid	$⊢ bday (n) \in suc bday (n)$
26		snssi	$⊢ bday (n) \in suc bday (n) \to \{bday (n)\} \subseteq suc bday (n)$
27	25 26	ax-mp	$⊢ \{bday (n)\} \subseteq suc bday (n)$
28	23 27	eqsstrdi	$⊢ n \in ℕ_{0s} \to bday [\{n\} \cup \emptyset] \subseteq suc bday (n)$
29		bdayelon	$⊢ bday (n) \in On$
30	29	onsuci	$⊢ suc bday (n) \in On$
31		scutbdaybnd	$⊢ (\{n\} ≪_{s} \emptyset \land suc bday (n) \in On \land bday [\{n\} \cup \emptyset] \subseteq suc bday (n)) \to bday (\{n\} \|_{s} \emptyset) \subseteq suc bday (n)$
32	30 31	mp3an2	$⊢ (\{n\} ≪_{s} \emptyset \land bday [\{n\} \cup \emptyset] \subseteq suc bday (n)) \to bday (\{n\} \|_{s} \emptyset) \subseteq suc bday (n)$
33	17 28 32	syl2anc	$⊢ n \in ℕ_{0s} \to bday (\{n\} \|_{s} \emptyset) \subseteq suc bday (n)$
34	13 33	eqsstrd	$⊢ n \in ℕ_{0s} \to bday (n +_{s} 1_{s}) \subseteq suc bday (n)$
35		bdayelon	$⊢ bday (n +_{s} 1_{s}) \in On$
36		onsssuc	$⊢ (bday (n +_{s} 1_{s}) \in On \land suc bday (n) \in On) \to (bday (n +_{s} 1_{s}) \subseteq suc bday (n) \leftrightarrow bday (n +_{s} 1_{s}) \in suc suc bday (n))$
37	35 30 36	mp2an	$⊢ bday (n +_{s} 1_{s}) \subseteq suc bday (n) \leftrightarrow bday (n +_{s} 1_{s}) \in suc suc bday (n)$
38	34 37	sylib	$⊢ n \in ℕ_{0s} \to bday (n +_{s} 1_{s}) \in suc suc bday (n)$
39		peano2	$⊢ bday (n) \in ω \to suc bday (n) \in ω$
40		peano2	$⊢ suc bday (n) \in ω \to suc suc bday (n) \in ω$
41	39 40	syl	$⊢ bday (n) \in ω \to suc suc bday (n) \in ω$
42		elnn	$⊢ (bday (n +_{s} 1_{s}) \in suc suc bday (n) \land suc suc bday (n) \in ω) \to bday (n +_{s} 1_{s}) \in ω$
43	38 41 42	syl2an	$⊢ (n \in ℕ_{0s} \land bday (n) \in ω) \to bday (n +_{s} 1_{s}) \in ω$
44	43	ex	$⊢ n \in ℕ_{0s} \to (bday (n) \in ω \to bday (n +_{s} 1_{s}) \in ω)$
45	2 4 6 8 11 44	n0sind	$⊢ A \in ℕ_{0s} \to bday (A) \in ω$

Metamath Proof Explorer

Theorem n0sbday

Proof