Theorem bdayon 27752

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 27649	. . 3 ⊢ bday : No –onto→On
2		fof 6747	. . 3 ⊢ ( bday : No –onto→On → bday : No ⟶On)
3	1, 2	ax-mp 5	. 2 ⊢ bday : No ⟶On
4		0elon 6373	. 2 ⊢ ∅ ∈ On
5	3, 4	f0cli 7045	1 ⊢ ( bday ‘𝐴) ∈ On

Syntax hints:   ∈ wcel 2114  Oncon0 6318  ⟶wf 6489  –onto→wfo 6491  ‘cfv 6493   No csur 27611   bday cbday 27613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-ord 6321  df-on 6322  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fo 6499  df-fv 6501  df-1o 8399  df-no 27614  df-bday 27616

This theorem is referenced by:  nocvxminlem  27754  cutbdaybnd2lim  27797  cutbdaylt  27798  lesrec  27799  bday1  27814  cuteq1  27817  leftf  27855  rightf  27856  madebdayim  27888  oldbdayim  27889  oldirr  27890  madebdaylemold  27898  madebdaylemlrcut  27899  madebday  27900  newbday  27902  lrcut  27904  0elold  27910  bdayiun  27915  cofcutr  27924  lrrecval2  27940  lrrecpo  27941  addsproplem2  27970  addsproplem4  27972  addsproplem5  27973  addsproplem6  27974  addsproplem7  27975  addsprop  27976  addbdaylem  28017  addbday  28018  negsproplem2  28029  negsproplem4  28031  negsproplem5  28032  negsproplem6  28033  negsproplem7  28034  negsprop  28035  negbdaylem  28056  negleft  28058  negright  28059  mulsproplem2  28117  mulsproplem3  28118  mulsproplem4  28119  mulsproplem5  28120  mulsproplem6  28121  mulsproplem7  28122  mulsproplem8  28123  mulsproplem12  28127  mulsproplem13  28128  mulsproplem14  28129  mulsprop  28130  ltonold  28261  oncutlt  28264  onnolt  28266  onlts  28267  onles  28268  oniso  28271  addonbday  28279  onsbnd  28281  onsbnd2  28282  n0bday  28352  onsfi  28356  bdayn0p1  28369  bdaypw2n0bndlem  28463  bdaypw2bnd  28465  bdayfinbndlem1  28467  z12bdaylem2  28471  z12bdaylem  28484