Theorem bdayon 28015

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

This proof depends on syntax axioms:   ∈ wcel 2145  Oncon0 6361  ⟶wf 6533  –onto→wfo 6535  ‘cfv 6537   No csur 27874   bday cbday 27876

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-ord 6364  df-on 6365  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fo 6543  df-fv 6545  df-1o 8458  df-no 27877  df-bday 27879

This theorem is used by:  nocvxminlem  28017  cutbdaybnd2lim  28060  cutbdaylt  28061  lesrec  28062  bday1  28077  cuteq1  28080  leftf  28118  rightf  28119  madebdayim  28151  oldbdayim  28152  oldirr  28153  madebdaylemold  28161  madebdaylemlrcut  28162  madebday  28163  newbday  28165  lrcut  28167  0elold  28173  bdayiun  28178  cofcutr  28187  lrrecval2  28203  lrrecpo  28204  addsproplem2  28233  addsproplem4  28235  addsproplem5  28236  addsproplem6  28237  addsproplem7  28238  addsprop  28239  addbdaylem  28280  addbday  28281  negsproplem2  28292  negsproplem4  28294  negsproplem5  28295  negsproplem6  28296  negsproplem7  28297  negsprop  28298  negbdaylem  28319  negleft  28321  negright  28322  mulsproplem2  28380  mulsproplem3  28381  mulsproplem4  28382  mulsproplem5  28383  mulsproplem6  28384  mulsproplem7  28385  mulsproplem8  28386  mulsproplem12  28390  mulsproplem13  28391  mulsproplem14  28392  mulsprop  28393  ltonold  28524  oncutlt  28527  onnolt  28529  onlts  28530  onles  28531  oniso  28534  addonbday  28542  onsbnd  28544  onsbnd2  28545  n0bday  28615  onsfi  28619  bdayn0p1  28632  bdaypw2n0bndlem  28726  bdaypw2bnd  28728  bdayfinbndlem1  28730  z12bdaylem2  28734  z12bdaylem  28747