Theorem nofun 27638

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

Syntax hints:   → wi 4   ∈ wcel 2119  ∃wrex 3064  {cpr 4564  Oncon0 6317  Fun wfun 6486  ⟶wf 6488  1_oc1o 8395  2_oc2o 8396   No csur 27628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-fun 6494  df-fn 6495  df-f 6496  df-no 27631

This theorem is referenced by:  nofnbday  27641  elno2  27643  nofv  27646  ltsres  27651  nosepon  27654  noextend  27655  noextendseq  27656  noextenddif  27657  noextendlt  27658  noextendgt  27659  nolesgn2ores  27661  nogesgn1ores  27663  nosepssdm  27675  nolt02olem  27683  nolt02o  27684  nogt01o  27685  nosupno  27692  nosupres  27696  nosupbnd1lem5  27701  nosupbnd1  27703  nosupbnd2lem1  27704  nosupbnd2  27705  noinfno  27707  noinfres  27711  noinfbnd1lem5  27716  noinfbnd1  27718  noinfbnd2lem1  27719  noinfbnd2  27720  noetasuplem2  27723  noetasuplem3  27724  noetasuplem4  27725  noetainflem2  27727  noetainflem4  27729