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