Theorem nofun 27988

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 27985	. 2 ⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
2		ffun 6704	. . 3 ⊢ (𝐴:𝑥⟶{1o, 2o} → Fun 𝐴)
3	2	rexlimivw 3160	. 2 ⊢ (∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o} → Fun 𝐴)
4	1, 3	sylbi 220	1 ⊢ (𝐴 ∈ No → Fun 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3087  {cpr 4586  Oncon0 6355  Fun wfun 6525  ⟶wf 6527  1_oc1o 8453  2_oc2o 8454   No csur 27979

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-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740

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-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6533  df-fn 6534  df-f 6535  df-no 27982

This theorem is used by:  nofnbday  27991  elno2  27993  nofv  27996  ltsres  28001  nosepon  28004  noextend  28005  noextendseq  28006  noextenddif  28007  noextendlt  28008  noextendgt  28009  nolesgn2ores  28011  nogesgn1ores  28013  nosepssdm  28025  nolt02olem  28033  nolt02o  28034  nogt01o  28035  nosupno  28042  nosupres  28046  nosupbnd1lem5  28051  nosupbnd1  28053  nosupbnd2lem1  28054  nosupbnd2  28055  noinfno  28057  noinfres  28061  noinfbnd1lem5  28066  noinfbnd1  28068  noinfbnd2lem1  28069  noinfbnd2  28070  noetasuplem2  28073  noetasuplem3  28074  noetasuplem4  28075  noetainflem2  28077  noetainflem4  28079