Theorem bdayon 27766

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

Syntax hints:   ∈ wcel 2121  Oncon0 6314  ⟶wf 6485  –onto→wfo 6487  ‘cfv 6489   No csur 27625   bday cbday 27627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-ord 6317  df-on 6318  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-fo 6495  df-fv 6497  df-1o 8399  df-no 27628  df-bday 27630

This theorem is referenced by:  nocvxminlem  27768  cutbdaybnd2lim  27811  cutbdaylt  27812  lesrec  27813  bday1  27828  cuteq1  27831  leftf  27869  rightf  27870  madebdayim  27902  oldbdayim  27903  oldirr  27904  madebdaylemold  27912  madebdaylemlrcut  27913  madebday  27914  newbday  27916  lrcut  27918  0elold  27924  bdayiun  27929  cofcutr  27938  lrrecval2  27954  lrrecpo  27955  addsproplem2  27984  addsproplem4  27986  addsproplem5  27987  addsproplem6  27988  addsproplem7  27989  addsprop  27990  addbdaylem  28031  addbday  28032  negsproplem2  28043  negsproplem4  28045  negsproplem5  28046  negsproplem6  28047  negsproplem7  28048  negsprop  28049  negbdaylem  28070  negleft  28072  negright  28073  mulsproplem2  28131  mulsproplem3  28132  mulsproplem4  28133  mulsproplem5  28134  mulsproplem6  28135  mulsproplem7  28136  mulsproplem8  28137  mulsproplem12  28141  mulsproplem13  28142  mulsproplem14  28143  mulsprop  28144  ltonold  28275  oncutlt  28278  onnolt  28280  onlts  28281  onles  28282  oniso  28285  addonbday  28293  onsbnd  28295  onsbnd2  28296  n0bday  28366  onsfi  28370  bdayn0p1  28383  bdaypw2n0bndlem  28477  bdaypw2bnd  28479  bdayfinbndlem1  28481  z12bdaylem2  28485  z12bdaylem  28498