Metamath Proof Explorer

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