bday1

Description: The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024)

		Ref	Expression
	Assertion	bday1	$⊢ bday (1_{s}) = 1_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		df-1s	$⊢ 1_{s} = \{0_{s}\} \|_{s} \emptyset$
2	1	fveq2i	$⊢ bday (1_{s}) = bday (\{0_{s}\} \|_{s} \emptyset)$
3		0no	$⊢ 0_{s} \in No$
4		snelpwi	$⊢ 0_{s} \in No \to \{0_{s}\} \in 𝒫 No$
5	3 4	ax-mp	$⊢ \{0_{s}\} \in 𝒫 No$
6		nulsgts	$⊢ \{0_{s}\} \in 𝒫 No \to \{0_{s}\} ≪_{s} \emptyset$
7	5 6	ax-mp	$⊢ \{0_{s}\} ≪_{s} \emptyset$
8		cutbdaybnd2	$⊢ \{0_{s}\} ≪_{s} \emptyset \to bday (\{0_{s}\} \|_{s} \emptyset) \subseteq suc ⋃ bday [\{0_{s}\} \cup \emptyset]$
9	7 8	ax-mp	$⊢ bday (\{0_{s}\} \|_{s} \emptyset) \subseteq suc ⋃ bday [\{0_{s}\} \cup \emptyset]$
10		un0	$⊢ \{0_{s}\} \cup \emptyset = \{0_{s}\}$
11	10	imaeq2i	$⊢ bday [\{0_{s}\} \cup \emptyset] = bday [\{0_{s}\}]$
12		bdayfn	$⊢ bday Fn No$
13		fnsnfv	$⊢ (bday Fn No \land 0_{s} \in No) \to \{bday (0_{s})\} = bday [\{0_{s}\}]$
14	12 3 13	mp2an	$⊢ \{bday (0_{s})\} = bday [\{0_{s}\}]$
15		bday0	$⊢ bday (0_{s}) = \emptyset$
16	15	sneqi	$⊢ \{bday (0_{s})\} = \{\emptyset\}$
17	11 14 16	3eqtr2i	$⊢ bday [\{0_{s}\} \cup \emptyset] = \{\emptyset\}$
18	17	unieqi	$⊢ ⋃ bday [\{0_{s}\} \cup \emptyset] = ⋃ \{\emptyset\}$
19		0ex	$⊢ \emptyset \in V$
20	19	unisn	$⊢ ⋃ \{\emptyset\} = \emptyset$
21	18 20	eqtri	$⊢ ⋃ bday [\{0_{s}\} \cup \emptyset] = \emptyset$
22		suceq	$⊢ ⋃ bday [\{0_{s}\} \cup \emptyset] = \emptyset \to suc ⋃ bday [\{0_{s}\} \cup \emptyset] = suc \emptyset$
23	21 22	ax-mp	$⊢ suc ⋃ bday [\{0_{s}\} \cup \emptyset] = suc \emptyset$
24		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
25	23 24	eqtr4i	$⊢ suc ⋃ bday [\{0_{s}\} \cup \emptyset] = 1_{𝑜}$
26	9 25	sseqtri	$⊢ bday (\{0_{s}\} \|_{s} \emptyset) \subseteq 1_{𝑜}$
27		ssrab2	$⊢ \{x \in No \| (\{0_{s}\} ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\} \subseteq No$
28		fnssintima	$⊢ (bday Fn No \land \{x \in No \| (\{0_{s}\} ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\} \subseteq No) \to (1_{𝑜} \subseteq ⋂ bday [\{x \in No \| (\{0_{s}\} ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\}] \leftrightarrow \forall y \in \{x \in No \| (\{0_{s}\} ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\} 1_{𝑜} \subseteq bday (y))$
29	12 27 28	mp2an	$⊢ 1_{𝑜} \subseteq ⋂ bday [\{x \in No \| (\{0_{s}\} ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\}] \leftrightarrow \forall y \in \{x \in No \| (\{0_{s}\} ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\} 1_{𝑜} \subseteq bday (y)$
30		sneq	$⊢ x = y \to \{x\} = \{y\}$
31	30	breq2d	$⊢ x = y \to (\{0_{s}\} ≪_{s} \{x\} \leftrightarrow \{0_{s}\} ≪_{s} \{y\})$
32	30	breq1d	$⊢ x = y \to (\{x\} ≪_{s} \emptyset \leftrightarrow \{y\} ≪_{s} \emptyset)$
33	31 32	anbi12d	$⊢ x = y \to ((\{0_{s}\} ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset) \leftrightarrow (\{0_{s}\} ≪_{s} \{y\} \land \{y\} ≪_{s} \emptyset))$
34	33	elrab	$⊢ y \in \{x \in No \| (\{0_{s}\} ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\} \leftrightarrow (y \in No \land (\{0_{s}\} ≪_{s} \{y\} \land \{y\} ≪_{s} \emptyset))$
35		ltsirr	$⊢ 0_{s} \in No \to \neg 0_{s} <_{s} 0_{s}$
36	3 35	ax-mp	$⊢ \neg 0_{s} <_{s} 0_{s}$
37		breq2	$⊢ y = 0_{s} \to (0_{s} <_{s} y \leftrightarrow 0_{s} <_{s} 0_{s})$
38	36 37	mtbiri	$⊢ y = 0_{s} \to \neg 0_{s} <_{s} y$
39	38	necon2ai	$⊢ 0_{s} <_{s} y \to y \neq 0_{s}$
40		bday0b	$⊢ y \in No \to (bday (y) = \emptyset \leftrightarrow y = 0_{s})$
41	40	necon3bid	$⊢ y \in No \to (bday (y) \neq \emptyset \leftrightarrow y \neq 0_{s})$
42	39 41	imbitrrid	$⊢ y \in No \to (0_{s} <_{s} y \to bday (y) \neq \emptyset)$
43		bdayon	$⊢ bday (y) \in On$
44	43	onordi	$⊢ Ord bday (y)$
45		ordge1n0	$⊢ Ord bday (y) \to (1_{𝑜} \subseteq bday (y) \leftrightarrow bday (y) \neq \emptyset)$
46	44 45	ax-mp	$⊢ 1_{𝑜} \subseteq bday (y) \leftrightarrow bday (y) \neq \emptyset$
47	42 46	imbitrrdi	$⊢ y \in No \to (0_{s} <_{s} y \to 1_{𝑜} \subseteq bday (y))$
48		sltssep	$⊢ \{0_{s}\} ≪_{s} \{y\} \to \forall x \in \{0_{s}\} \forall z \in \{y\} x <_{s} z$
49		vex	$⊢ y \in V$
50		breq2	$⊢ z = y \to (x <_{s} z \leftrightarrow x <_{s} y)$
51	49 50	ralsn	$⊢ \forall z \in \{y\} x <_{s} z \leftrightarrow x <_{s} y$
52	51	ralbii	$⊢ \forall x \in \{0_{s}\} \forall z \in \{y\} x <_{s} z \leftrightarrow \forall x \in \{0_{s}\} x <_{s} y$
53	3	elexi	$⊢ 0_{s} \in V$
54		breq1	$⊢ x = 0_{s} \to (x <_{s} y \leftrightarrow 0_{s} <_{s} y)$
55	53 54	ralsn	$⊢ \forall x \in \{0_{s}\} x <_{s} y \leftrightarrow 0_{s} <_{s} y$
56	52 55	bitri	$⊢ \forall x \in \{0_{s}\} \forall z \in \{y\} x <_{s} z \leftrightarrow 0_{s} <_{s} y$
57	48 56	sylib	$⊢ \{0_{s}\} ≪_{s} \{y\} \to 0_{s} <_{s} y$
58	47 57	impel	$⊢ (y \in No \land \{0_{s}\} ≪_{s} \{y\}) \to 1_{𝑜} \subseteq bday (y)$
59	58	adantrr	$⊢ (y \in No \land (\{0_{s}\} ≪_{s} \{y\} \land \{y\} ≪_{s} \emptyset)) \to 1_{𝑜} \subseteq bday (y)$
60	34 59	sylbi	$⊢ y \in \{x \in No \| (\{0_{s}\} ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\} \to 1_{𝑜} \subseteq bday (y)$
61	29 60	mprgbir	$⊢ 1_{𝑜} \subseteq ⋂ bday [\{x \in No \| (\{0_{s}\} ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\}]$
62		cutbday	$⊢ \{0_{s}\} ≪_{s} \emptyset \to bday (\{0_{s}\} \|_{s} \emptyset) = ⋂ bday [\{x \in No \| (\{0_{s}\} ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\}]$
63	7 62	ax-mp	$⊢ bday (\{0_{s}\} \|_{s} \emptyset) = ⋂ bday [\{x \in No \| (\{0_{s}\} ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\}]$
64	61 63	sseqtrri	$⊢ 1_{𝑜} \subseteq bday (\{0_{s}\} \|_{s} \emptyset)$
65	26 64	eqssi	$⊢ bday (\{0_{s}\} \|_{s} \emptyset) = 1_{𝑜}$
66	2 65	eqtri	$⊢ bday (1_{s}) = 1_{𝑜}$

Metamath Proof Explorer

Theorem bday1

Proof