Metamath Proof Explorer

Theorem bdayrn

Description: The birthday function's range is On . (Contributed by Scott Fenton, 14-Jun-2011)

Ref Expression
Assertion bdayrn 
|- ran bday = On

Proof

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