bdayfo

Description: The birthday function maps the surreals onto the ordinals. Axiom B of Alling p. 184. (Proof shortened on 14-Apr-2012 by SF). (Contributed by Scott Fenton, 11-Jun-2011)

		Ref	Expression
	Assertion	bdayfo	$⊢ bday : No \underset{onto}{⟶} On$

Proof

Step	Hyp	Ref	Expression
1		dmexg	$⊢ x \in No \to dom x \in V$
2	1	rgen	$⊢ \forall x \in No dom x \in V$
3		df-bday	$⊢ bday = (x \in No ⟼ dom x)$
4	3	mptfng	$⊢ \forall x \in No dom x \in V \leftrightarrow bday Fn No$
5	2 4	mpbi	$⊢ bday Fn No$
6	3	rnmpt	$⊢ ran bday = \{y \| \exists x \in No y = dom x\}$
7		noxp1o	$⊢ y \in On \to y \times \{1_{𝑜}\} \in No$
8		1oex	$⊢ 1_{𝑜} \in V$
9	8	snnz	$⊢ \{1_{𝑜}\} \neq \emptyset$
10		dmxp	$⊢ \{1_{𝑜}\} \neq \emptyset \to dom (y \times \{1_{𝑜}\}) = y$
11	9 10	ax-mp	$⊢ dom (y \times \{1_{𝑜}\}) = y$
12	11	eqcomi	$⊢ y = dom (y \times \{1_{𝑜}\})$
13		dmeq	$⊢ x = y \times \{1_{𝑜}\} \to dom x = dom (y \times \{1_{𝑜}\})$
14	13	rspceeqv	$⊢ (y \times \{1_{𝑜}\} \in No \land y = dom (y \times \{1_{𝑜}\})) \to \exists x \in No y = dom x$
15	7 12 14	sylancl	$⊢ y \in On \to \exists x \in No y = dom x$
16		nodmon	$⊢ x \in No \to dom x \in On$
17		eleq1a	$⊢ dom x \in On \to (y = dom x \to y \in On)$
18	16 17	syl	$⊢ x \in No \to (y = dom x \to y \in On)$
19	18	rexlimiv	$⊢ \exists x \in No y = dom x \to y \in On$
20	15 19	impbii	$⊢ y \in On \leftrightarrow \exists x \in No y = dom x$
21	20	eqabi	$⊢ On = \{y \| \exists x \in No y = dom x\}$
22	6 21	eqtr4i	$⊢ ran bday = On$
23		df-fo	$⊢ bday : No \underset{onto}{⟶} On \leftrightarrow (bday Fn No \land ran bday = On)$
24	5 22 23	mpbir2an	$⊢ bday : No \underset{onto}{⟶} On$

Metamath Proof Explorer

Theorem bdayfo

Proof