Metamath Proof Explorer

Theorem bdaydm

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

Ref Expression
Assertion bdaydm 
|- dom bday = No

Proof

Step Hyp Ref Expression
1 bdayfo 
 |-  bday : No -onto-> On
2 fof 
 |-  ( bday : No -onto-> On -> bday : No --> On )
3 1 2 ax-mp 
 |-  bday : No --> On
4 3 fdmi 
 |-  dom bday = No