Theorem bdayon 28138

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

This proof depends on syntax axioms:   ∈ wcel 2144  Oncon0 6362  ⟶wf 6534  –onto→wfo 6536  ‘cfv 6538  Nocsur 27997  bdaycbday 27999

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-ord 6365  df-on 6366  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fo 6544  df-fv 6546  df-1o 8476  df-no 28000  df-bday 28002

This theorem is used by:  nocvxminlem  28140  cutbdaybnd2lim  28183  cutbdaylt  28184  lesrec  28185  bday1  28200  cuteq1  28203  leftf  28241  rightf  28242  madebdayim  28274  oldbdayim  28275  oldirr  28276  madebdaylemold  28284  madebdaylemlrcut  28285  madebday  28286  newbday  28288  lrcut  28290  0elold  28296  bdayiun  28301  cofcutr  28310  lrrecval2  28326  lrrecpo  28327  addsproplem2  28356  addsproplem4  28358  addsproplem5  28359  addsproplem6  28360  addsproplem7  28361  addsprop  28362  addbdaylem  28403  addbday  28404  negsproplem2  28415  negsproplem4  28417  negsproplem5  28418  negsproplem6  28419  negsproplem7  28420  negsprop  28421  negbdaylem  28442  negleft  28444  negright  28445  mulsproplem2  28503  mulsproplem3  28504  mulsproplem4  28505  mulsproplem5  28506  mulsproplem6  28507  mulsproplem7  28508  mulsproplem8  28509  mulsproplem12  28513  mulsproplem13  28514  mulsproplem14  28515  mulsprop  28516  ltonold  28647  oncutlt  28650  onnolt  28652  onlts  28653  onles  28654  oniso  28657  addonbday  28665  onsbnd  28667  onsbnd2  28668  n0bday  28738  onsfi  28742  bdayn0p1  28755  bdaypw2n0bndlem  28849  bdaypw2bnd  28851  bdayfinbndlem1  28853  z12bdaylem2  28857  z12bdaylem  28870