Theorem bdayelon 27688

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

Syntax hints:   ∈ wcel 2109  Oncon0 6332  ⟶wf 6507  –onto→wfo 6509  ‘cfv 6511   No csur 27551   bday cbday 27553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-ord 6335  df-on 6336  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fo 6517  df-fv 6519  df-1o 8434  df-no 27554  df-bday 27556

This theorem is referenced by:  nocvxminlem  27689  scutbdaybnd2lim  27729  scutbdaylt  27730  slerec  27731  bday1s  27743  cuteq1  27746  leftf  27777  rightf  27778  madebdayim  27799  oldbdayim  27800  oldirr  27801  madebdaylemold  27809  madebdaylemlrcut  27810  madebday  27811  newbday  27813  lrcut  27815  0elold  27821  cofcutr  27832  lrrecval2  27847  lrrecpo  27848  addsproplem2  27877  addsproplem4  27879  addsproplem5  27880  addsproplem6  27881  addsproplem7  27882  addsprop  27883  addsbdaylem  27923  addsbday  27924  negsproplem2  27935  negsproplem4  27937  negsproplem5  27938  negsproplem6  27939  negsproplem7  27940  negsprop  27941  negsbdaylem  27962  mulsproplem2  28020  mulsproplem3  28021  mulsproplem4  28022  mulsproplem5  28023  mulsproplem6  28024  mulsproplem7  28025  mulsproplem8  28026  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  mulsprop  28033  sltonold  28162  onscutlt  28165  onnolt  28167  onslt  28168  onsiso  28169  n0sbday  28244  onsfi  28247  bdayn0p1  28258  zs12bday  28343