Theorem bdayfn

Description: The birthday function is a function over No . (Contributed by Scott Fenton, 30-Jun-2011)

	Ref	Expression
Assertion	bdayfn	⊢ bday Fn No

Proof

Step	Hyp	Ref	Expression
1		bdayfo	⊢ bday : No –onto→ On
2		fofn	⊢ ( bday : No –onto→ On → bday Fn No )
3	1 2	ax-mp	⊢ bday Fn No