Metamath Proof Explorer


Theorem bdayfun

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

Ref Expression
Assertion bdayfun
|- Fun bday

Proof

Step Hyp Ref Expression
1 bdayfo
 |-  bday : No -onto-> On
2 fofun
 |-  ( bday : No -onto-> On -> Fun bday )
3 1 2 ax-mp
 |-  Fun bday