Theorem nofun 28012

Description: A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011.)

Assertion

Ref	Expression
nofun	⊢ (𝐴 ∈ No → Fun 𝐴)

Proof of Theorem nofun

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elno 28009	. 2 ⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
2		ffun 6713	. . 3 ⊢ (𝐴:𝑥⟶{1o, 2o} → Fun 𝐴)
3	2	rexlimivw 3159	. 2 ⊢ (∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o} → Fun 𝐴)
4	1, 3	sylbi 220	1 ⊢ (𝐴 ∈ No → Fun 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∃wrex 3086  {cpr 4586  Oncon0 6362  Fun wfun 6533  ⟶wf 6535  1_oc1o 8473  2_oc2o 8474  Nocsur 28003

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6541  df-fn 6542  df-f 6543  df-no 28006

This theorem is used by:  nofnbday  28015  elno2  28017  nofv  28020  ltsres  28025  nosepon  28028  noextend  28029  noextendseq  28030  noextenddif  28031  noextendlt  28032  noextendgt  28033  nolesgn2ores  28035  nogesgn1ores  28037  nosepssdm  28049  nolt02olem  28057  nolt02o  28058  nogt01o  28059  nosupno  28066  nosupres  28070  nosupbnd1lem5  28075  nosupbnd1  28077  nosupbnd2lem1  28078  nosupbnd2  28079  noinfno  28081  noinfres  28085  noinfbnd1lem5  28090  noinfbnd1  28092  noinfbnd2lem1  28093  noinfbnd2  28094  noetasuplem2  28097  noetasuplem3  28098  noetasuplem4  28099  noetainflem2  28101  noetainflem4  28103