Theorem bdayon 28057

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

This proof depends on syntax axioms:   ∈ wcel 2145  Oncon0 6352  ⟶wf 6524  –onto→wfo 6526  ‘cfv 6528   No csur 27916   bday cbday 27918

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 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735

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 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-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5543  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-ord 6355  df-on 6356  df-suc 6358  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-fo 6534  df-fv 6536  df-1o 8455  df-no 27919  df-bday 27921

This theorem is used by:  nocvxminlem  28059  cutbdaybnd2lim  28102  cutbdaylt  28103  lesrec  28104  bday1  28119  cuteq1  28122  leftf  28160  rightf  28161  madebdayim  28193  oldbdayim  28194  oldirr  28195  madebdaylemold  28203  madebdaylemlrcut  28204  madebday  28205  newbday  28207  lrcut  28209  0elold  28215  bdayiun  28220  cofcutr  28229  lrrecval2  28245  lrrecpo  28246  addsproplem2  28275  addsproplem4  28277  addsproplem5  28278  addsproplem6  28279  addsproplem7  28280  addsprop  28281  addbdaylem  28322  addbday  28323  negsproplem2  28334  negsproplem4  28336  negsproplem5  28337  negsproplem6  28338  negsproplem7  28339  negsprop  28340  negbdaylem  28361  negleft  28363  negright  28364  mulsproplem2  28422  mulsproplem3  28423  mulsproplem4  28424  mulsproplem5  28425  mulsproplem6  28426  mulsproplem7  28427  mulsproplem8  28428  mulsproplem12  28432  mulsproplem13  28433  mulsproplem14  28434  mulsprop  28435  ltonold  28566  oncutlt  28569  onnolt  28571  onlts  28572  onles  28573  oniso  28576  addonbday  28584  onsbnd  28586  onsbnd2  28587  n0bday  28657  onsfi  28661  bdayn0p1  28674  bdaypw2n0bndlem  28768  bdaypw2bnd  28770  bdayfinbndlem1  28772  z12bdaylem2  28776  z12bdaylem  28789