Theorem bdaydm

Description: The birthday function's domain is No . (Contributed by Scott Fenton, 14-Jun-2011) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

	Ref	Expression
Assertion	bdaydm	$$⊢\mathrm{dom}\mathrm{bday}=\mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		bdayfn	$$⊢\mathrm{bday}Fn\mathrm{No}$$
2	1	fndmi	$$⊢\mathrm{dom}\mathrm{bday}=\mathrm{No}$$