Theorem bdayfo

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

	Ref	Expression
Assertion	bdayfo	⊢ bday : No –onto→ On

Proof

Step	Hyp	Ref	Expression
1		dmexg	⊢ ( 𝑥 ∈ No → dom 𝑥 ∈ V )
2	1	rgen	⊢ ∀ 𝑥 ∈ No dom 𝑥 ∈ V
3		df-bday	⊢ bday = ( 𝑥 ∈ No ↦ dom 𝑥 )
4	3	mptfng	⊢ ( ∀ 𝑥 ∈ No dom 𝑥 ∈ V ↔ bday Fn No )
5	2 4	mpbi	⊢ bday Fn No
6	3	rnmpt	⊢ ran bday = { 𝑦 ∣ ∃ 𝑥 ∈ No 𝑦 = dom 𝑥 }
7		noxp1o	⊢ ( 𝑦 ∈ On → ( 𝑦 × { 1o } ) ∈ No )
8		1oex	⊢ 1o ∈ V
9	8	snnz	⊢ { 1o } ≠ ∅
10		dmxp	⊢ ( { 1o } ≠ ∅ → dom ( 𝑦 × { 1o } ) = 𝑦 )
11	9 10	ax-mp	⊢ dom ( 𝑦 × { 1o } ) = 𝑦
12	11	eqcomi	⊢ 𝑦 = dom ( 𝑦 × { 1o } )
13		dmeq	⊢ ( 𝑥 = ( 𝑦 × { 1o } ) → dom 𝑥 = dom ( 𝑦 × { 1o } ) )
14	13	rspceeqv	⊢ ( ( ( 𝑦 × { 1o } ) ∈ No ∧ 𝑦 = dom ( 𝑦 × { 1o } ) ) → ∃ 𝑥 ∈ No 𝑦 = dom 𝑥 )
15	7 12 14	sylancl	⊢ ( 𝑦 ∈ On → ∃ 𝑥 ∈ No 𝑦 = dom 𝑥 )
16		nodmon	⊢ ( 𝑥 ∈ No → dom 𝑥 ∈ On )
17		eleq1a	⊢ ( dom 𝑥 ∈ On → ( 𝑦 = dom 𝑥 → 𝑦 ∈ On ) )
18	16 17	syl	⊢ ( 𝑥 ∈ No → ( 𝑦 = dom 𝑥 → 𝑦 ∈ On ) )
19	18	rexlimiv	⊢ ( ∃ 𝑥 ∈ No 𝑦 = dom 𝑥 → 𝑦 ∈ On )
20	15 19	impbii	⊢ ( 𝑦 ∈ On ↔ ∃ 𝑥 ∈ No 𝑦 = dom 𝑥 )
21	20	abbi2i	⊢ On = { 𝑦 ∣ ∃ 𝑥 ∈ No 𝑦 = dom 𝑥 }
22	6 21	eqtr4i	⊢ ran bday = On
23		df-fo	⊢ ( bday : No –onto→ On ↔ ( bday Fn No ∧ ran bday = On ) )
24	5 22 23	mpbir2an	⊢ bday : No –onto→ On