Theorem nofun 27589

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3057  {cpr 4577  Oncon0 6311  Fun wfun 6480  ⟶wf 6482  1_oc1o 8384  2_oc2o 8385   No csur 27579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-fun 6488  df-fn 6489  df-f 6490  df-no 27582

This theorem is referenced by:  nofnbday  27592  elno2  27594  nofv  27597  sltres  27602  nosepon  27605  noextend  27606  noextendseq  27607  noextenddif  27608  noextendlt  27609  noextendgt  27610  nolesgn2ores  27612  nogesgn1ores  27614  nosepssdm  27626  nolt02olem  27634  nolt02o  27635  nogt01o  27636  nosupno  27643  nosupres  27647  nosupbnd1lem5  27652  nosupbnd1  27654  nosupbnd2lem1  27655  nosupbnd2  27656  noinfno  27658  noinfres  27662  noinfbnd1lem5  27667  noinfbnd1  27669  noinfbnd2lem1  27670  noinfbnd2  27671  noetasuplem2  27674  noetasuplem3  27675  noetasuplem4  27676  noetainflem2  27678  noetainflem4  27680