Theorem nofun 27850

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∃wrex 3092  {cpr 4596  Oncon0 6367  Fun wfun 6537  ⟶wf 6539  1_oc1o 8455  2_oc2o 8456   No csur 27841

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-pr 5409  ax-un 7745

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-fun 6545  df-fn 6546  df-f 6547  df-no 27844

This theorem is used by:  nofnbday  27853  elno2  27855  nofv  27858  ltsres  27863  nosepon  27866  noextend  27867  noextendseq  27868  noextenddif  27869  noextendlt  27870  noextendgt  27871  nolesgn2ores  27873  nogesgn1ores  27875  nosepssdm  27887  nolt02olem  27895  nolt02o  27896  nogt01o  27897  nosupno  27904  nosupres  27908  nosupbnd1lem5  27913  nosupbnd1  27915  nosupbnd2lem1  27916  nosupbnd2  27917  noinfno  27919  noinfres  27923  noinfbnd1lem5  27928  noinfbnd1  27930  noinfbnd2lem1  27931  noinfbnd2  27932  noetasuplem2  27935  noetasuplem3  27936  noetasuplem4  27937  noetainflem2  27939  noetainflem4  27941