Theorem bdayon 28165

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 28061	. . 3 ⊢ bday:No⟶ontoOn
2		fof 6815	. . 3 ⊢ (bday:No⟶ontoOn → bday:No⟶On)
3	1, 2	ax-mp 5	. 2 ⊢ bday:No⟶On
4		0elon 6433	. 2 ⊢ ∅ ∈ On
5	3, 4	f0cli 7119	1 ⊢ (bday‘𝐴) ∈ On

This proof depends on syntax axioms:   ∈ wcel 2147  Oncon0 6377  ⟶wf 6551  ⟶ontowfo 6553  ‘cfv 6555  Nocsur 28024  bdaycbday 28026

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-ord 6380  df-on 6381  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-fo 6561  df-fv 6563  df-1o 8501  df-no 28027  df-bday 28029

This theorem is used by:  nocvxminlem  28167  cutbdaybnd2lim  28210  cutbdaylt  28211  lesrec  28212  bday1  28227  cuteq1  28230  leftf  28268  rightf  28269  madebdayim  28301  oldbdayim  28302  oldirr  28303  madebdaylemold  28311  madebdaylemlrcut  28312  madebday  28313  newbday  28315  lrcut  28317  0elold  28323  bdayiun  28328  cofcutr  28337  lrrecval2  28353  lrrecpo  28354  addsproplem2  28383  addsproplem4  28385  addsproplem5  28386  addsproplem6  28387  addsproplem7  28388  addsprop  28389  addbdaylem  28430  addbday  28431  negsproplem2  28442  negsproplem4  28444  negsproplem5  28445  negsproplem6  28446  negsproplem7  28447  negsprop  28448  negbdaylem  28469  negleft  28471  negright  28472  mulsproplem2  28530  mulsproplem3  28531  mulsproplem4  28532  mulsproplem5  28533  mulsproplem6  28534  mulsproplem7  28535  mulsproplem8  28536  mulsproplem12  28540  mulsproplem13  28541  mulsproplem14  28542  mulsprop  28543  ltonold  28674  oncutlt  28677  onnolt  28679  onlts  28680  onles  28681  oniso  28684  addonbday  28692  onsbnd  28694  onsbnd2  28695  n0bday  28765  onsfi  28769  bdayn0p1  28782  bdaypw2n0bndlem  28876  bdaypw2bnd  28878  bdayfinbndlem1  28880  z12bdaylem2  28884  z12bdaylem  28897