Theorem bdayelon 27716

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.)

Assertion

Ref	Expression
bdayelon	⊢ ( bday ‘𝐴) ∈ On

Proof of Theorem bdayelon

Step	Hyp	Ref	Expression
1		bdayfo 27617	. . 3 ⊢ bday : No –onto→On
2		fof 6735	. . 3 ⊢ ( bday : No –onto→On → bday : No ⟶On)
3	1, 2	ax-mp 5	. 2 ⊢ bday : No ⟶On
4		0elon 6361	. 2 ⊢ ∅ ∈ On
5	3, 4	f0cli 7031	1 ⊢ ( bday ‘𝐴) ∈ On

Syntax hints:   ∈ wcel 2111  Oncon0 6306  ⟶wf 6477  –onto→wfo 6479  ‘cfv 6481   No csur 27579   bday cbday 27581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-ord 6309  df-on 6310  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fo 6487  df-fv 6489  df-1o 8385  df-no 27582  df-bday 27584

This theorem is referenced by:  nocvxminlem  27718  scutbdaybnd2lim  27759  scutbdaylt  27760  slerec  27761  bday1s  27776  cuteq1  27779  leftf  27811  rightf  27812  madebdayim  27834  oldbdayim  27835  oldirr  27836  madebdaylemold  27844  madebdaylemlrcut  27845  madebday  27846  newbday  27848  lrcut  27850  0elold  27856  bdayiun  27861  cofcutr  27869  lrrecval2  27884  lrrecpo  27885  addsproplem2  27914  addsproplem4  27916  addsproplem5  27917  addsproplem6  27918  addsproplem7  27919  addsprop  27920  addsbdaylem  27960  addsbday  27961  negsproplem2  27972  negsproplem4  27974  negsproplem5  27975  negsproplem6  27976  negsproplem7  27977  negsprop  27978  negsbdaylem  27999  mulsproplem2  28057  mulsproplem3  28058  mulsproplem4  28059  mulsproplem5  28060  mulsproplem6  28061  mulsproplem7  28062  mulsproplem8  28063  mulsproplem12  28067  mulsproplem13  28068  mulsproplem14  28069  mulsprop  28070  sltonold  28199  onscutlt  28202  onnolt  28204  onslt  28205  onsiso  28206  n0sbday  28281  onsfi  28284  bdayn0p1  28295  zs12bday  28395