Theorem bdayelon

Description: The value of the birthday function is always an ordinal. (Contributed by Scott Fenton, 14-Jun-2011) (Proof shortened by Scott Fenton, 8-Dec-2021)

	Ref	Expression
Assertion	bdayelon	⊢ ( bday ‘ 𝐴 ) ∈ On

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		0elon	⊢ ∅ ∈ On
5	3 4	f0cli	⊢ ( bday ‘ 𝐴 ) ∈ On