Theorem bdayfn 27758

Description: The birthday function is a function over No . (Contributed by Scott Fenton, 30-Jun-2011.)

Assertion

Ref	Expression
bdayfn	⊢ bday Fn No

Proof of Theorem bdayfn

Step	Hyp	Ref	Expression
1		bdayfo 27658	. 2 ⊢ bday : No –onto→On
2		fofn 6749	. 2 ⊢ ( bday : No –onto→On → bday Fn No )
3	1, 2	ax-mp 5	1 ⊢ bday Fn No

Syntax hints:  Oncon0 6318   Fn wfn 6488  –onto→wfo 6491   No csur 27620   bday cbday 27622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pow 5303  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-suc 6324  df-fun 6495  df-fn 6496  df-f 6497  df-fo 6499  df-1o 8399  df-no 27623  df-bday 27625

This theorem is referenced by:  nobdaymin  27762  eqcuts2  27795  cutsun12  27799  cutbdaybnd  27804  cutbdaybnd2  27805  cutbdaylt  27807  bday1  27823  cuteq0  27824  madebdaylemlrcut  27908  sltsbday  27926  cofcut1  27929  cofcutr  27933  lrrecfr  27952  oniso  28280  bdayons  28285  n0bday  28361  bdayn0p1  28378  bdaypw2n0bndlem  28472