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		peano2n0s	$⊢ n \in ℕ_{0s} \to n +_{s} 1_{s} \in ℕ_{0s}$
13		n0scut	$⊢ n +_{s} 1_{s} \in ℕ_{0s} \to n +_{s} 1_{s} = \{(n +_{s} 1_{s}) -_{s} 1_{s}\} \|_{s} \emptyset$
14	12 13	syl	$⊢ n \in ℕ_{0s} \to n +_{s} 1_{s} = \{(n +_{s} 1_{s}) -_{s} 1_{s}\} \|_{s} \emptyset$
15		n0sno	$⊢ n \in ℕ_{0s} \to n \in No$
16		1sno	$⊢ 1_{s} \in No$
17		pncans	$⊢ (n \in No \land 1_{s} \in No) \to (n +_{s} 1_{s}) -_{s} 1_{s} = n$
18	15 16 17	sylancl	$⊢ n \in ℕ_{0s} \to (n +_{s} 1_{s}) -_{s} 1_{s} = n$
19	18	sneqd	$⊢ n \in ℕ_{0s} \to \{(n +_{s} 1_{s}) -_{s} 1_{s}\} = \{n\}$
20	19	oveq1d	$⊢ n \in ℕ_{0s} \to \{(n +_{s} 1_{s}) -_{s} 1_{s}\} \|_{s} \emptyset = \{n\} \|_{s} \emptyset$
21	14 20	eqtrd	$⊢ n \in ℕ_{0s} \to n +_{s} 1_{s} = \{n\} \|_{s} \emptyset$
22	21	fveq2d	$⊢ n \in ℕ_{0s} \to bday (n +_{s} 1_{s}) = bday (\{n\} \|_{s} \emptyset)$
23		snelpwi	$⊢ n \in No \to \{n\} \in 𝒫 No$
24		nulssgt	$⊢ \{n\} \in 𝒫 No \to \{n\} ≪_{s} \emptyset$
25	15 23 24	3syl	$⊢ n \in ℕ_{0s} \to \{n\} ≪_{s} \emptyset$
26		un0	$⊢ \{n\} \cup \emptyset = \{n\}$
27	26	imaeq2i	$⊢ bday [\{n\} \cup \emptyset] = bday [\{n\}]$
28		bdayfn	$⊢ bday Fn No$
29		fnsnfv	$⊢ (bday Fn No \land n \in No) \to \{bday (n)\} = bday [\{n\}]$
30	28 15 29	sylancr	$⊢ n \in ℕ_{0s} \to \{bday (n)\} = bday [\{n\}]$
31	27 30	eqtr4id	$⊢ n \in ℕ_{0s} \to bday [\{n\} \cup \emptyset] = \{bday (n)\}$
32		fvex	$⊢ bday (n) \in V$
33	32	sucid	$⊢ bday (n) \in suc bday (n)$
34		snssi	$⊢ bday (n) \in suc bday (n) \to \{bday (n)\} \subseteq suc bday (n)$
35	33 34	ax-mp	$⊢ \{bday (n)\} \subseteq suc bday (n)$
36	31 35	eqsstrdi	$⊢ n \in ℕ_{0s} \to bday [\{n\} \cup \emptyset] \subseteq suc bday (n)$
37		bdayelon	$⊢ bday (n) \in On$
38	37	onsuci	$⊢ suc bday (n) \in On$
39		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)$
40	38 39	mp3an2	$⊢ (\{n\} ≪_{s} \emptyset \land bday [\{n\} \cup \emptyset] \subseteq suc bday (n)) \to bday (\{n\} \|_{s} \emptyset) \subseteq suc bday (n)$
41	25 36 40	syl2anc	$⊢ n \in ℕ_{0s} \to bday (\{n\} \|_{s} \emptyset) \subseteq suc bday (n)$
42	22 41	eqsstrd	$⊢ n \in ℕ_{0s} \to bday (n +_{s} 1_{s}) \subseteq suc bday (n)$
43		bdayelon	$⊢ bday (n +_{s} 1_{s}) \in On$
44		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))$
45	43 38 44	mp2an	$⊢ bday (n +_{s} 1_{s}) \subseteq suc bday (n) \leftrightarrow bday (n +_{s} 1_{s}) \in suc suc bday (n)$
46	42 45	sylib	$⊢ n \in ℕ_{0s} \to bday (n +_{s} 1_{s}) \in suc suc bday (n)$
47		peano2	$⊢ bday (n) \in ω \to suc bday (n) \in ω$
48		peano2	$⊢ suc bday (n) \in ω \to suc suc bday (n) \in ω$
49	47 48	syl	$⊢ bday (n) \in ω \to suc suc bday (n) \in ω$
50		elnn	$⊢ (bday (n +_{s} 1_{s}) \in suc suc bday (n) \land suc suc bday (n) \in ω) \to bday (n +_{s} 1_{s}) \in ω$
51	46 49 50	syl2an	$⊢ (n \in ℕ_{0s} \land bday (n) \in ω) \to bday (n +_{s} 1_{s}) \in ω$
52	51	ex	$⊢ n \in ℕ_{0s} \to (bday (n) \in ω \to bday (n +_{s} 1_{s}) \in ω)$
53	2 4 6 8 11 52	n0sind	$⊢ A \in ℕ_{0s} \to bday (A) \in ω$

Metamath Proof Explorer

Theorem n0sbday

Proof