Theorem bdayon 27847

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
bdayon	⊢ ( bday ‘𝐴) ∈ On

Proof of Theorem bdayon

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

Syntax hints:   ∈ wcel 2144  Oncon0 6348  ⟶wf 6519  –onto→wfo 6521  ‘cfv 6523   No csur 27706   bday cbday 27708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-ord 6351  df-on 6352  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-fo 6529  df-fv 6531  df-1o 8439  df-no 27709  df-bday 27711

This theorem is referenced by:  nocvxminlem  27849  cutbdaybnd2lim  27892  cutbdaylt  27893  lesrec  27894  bday1  27909  cuteq1  27912  leftf  27950  rightf  27951  madebdayim  27983  oldbdayim  27984  oldirr  27985  madebdaylemold  27993  madebdaylemlrcut  27994  madebday  27995  newbday  27997  lrcut  27999  0elold  28005  bdayiun  28010  cofcutr  28019  lrrecval2  28035  lrrecpo  28036  addsproplem2  28065  addsproplem4  28067  addsproplem5  28068  addsproplem6  28069  addsproplem7  28070  addsprop  28071  addbdaylem  28112  addbday  28113  negsproplem2  28124  negsproplem4  28126  negsproplem5  28127  negsproplem6  28128  negsproplem7  28129  negsprop  28130  negbdaylem  28151  negleft  28153  negright  28154  mulsproplem2  28212  mulsproplem3  28213  mulsproplem4  28214  mulsproplem5  28215  mulsproplem6  28216  mulsproplem7  28217  mulsproplem8  28218  mulsproplem12  28222  mulsproplem13  28223  mulsproplem14  28224  mulsprop  28225  ltonold  28356  oncutlt  28359  onnolt  28361  onlts  28362  onles  28363  oniso  28366  addonbday  28374  onsbnd  28376  onsbnd2  28377  n0bday  28447  onsfi  28451  bdayn0p1  28464  bdaypw2n0bndlem  28558  bdaypw2bnd  28560  bdayfinbndlem1  28562  z12bdaylem2  28566  z12bdaylem  28579