Metamath Proof Explorer

Theorem nofun

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

Ref Expression
Assertion nofun 
|- ( A e. No -> Fun A )

Proof

Step Hyp Ref Expression
1 elno 
 |-  ( A e. No <-> E. x e. On A : x --> { 1o , 2o } )
2 ffun 
 |-  ( A : x --> { 1o , 2o } -> Fun A )
3 2 rexlimivw 
 |-  ( E. x e. On A : x --> { 1o , 2o } -> Fun A )
4 1 3 sylbi 
 |-  ( A e. No -> Fun A )