Theorem nofv

Description: The function value of a surreal is either a sign or the empty set. (Contributed by Scott Fenton, 22-Jun-2011)

	Ref	Expression
Assertion	nofv	|- ( A e. No -> ( ( A ` X ) = (/) \/ ( A ` X ) = 1o \/ ( A ` X ) = 2o ) )

Proof

Step	Hyp	Ref	Expression
1		pm2.1	|- ( -. X e. dom A \/ X e. dom A )
2		ndmfv	|- ( -. X e. dom A -> ( A ` X ) = (/) )
3	2	a1i	|- ( A e. No -> ( -. X e. dom A -> ( A ` X ) = (/) ) )
4		nofun	|- ( A e. No -> Fun A )
5		norn	|- ( A e. No -> ran A C_ { 1o , 2o } )
6		fvelrn	|- ( ( Fun A /\ X e. dom A ) -> ( A ` X ) e. ran A )
7		ssel	|- ( ran A C_ { 1o , 2o } -> ( ( A ` X ) e. ran A -> ( A ` X ) e. { 1o , 2o } ) )
8	6 7	syl5com	|- ( ( Fun A /\ X e. dom A ) -> ( ran A C_ { 1o , 2o } -> ( A ` X ) e. { 1o , 2o } ) )
9	8	impancom	|- ( ( Fun A /\ ran A C_ { 1o , 2o } ) -> ( X e. dom A -> ( A ` X ) e. { 1o , 2o } ) )
10		1oex	|- 1o e. _V
11		2on	|- 2o e. On
12	11	elexi	|- 2o e. _V
13	10 12	elpr2	|- ( ( A ` X ) e. { 1o , 2o } <-> ( ( A ` X ) = 1o \/ ( A ` X ) = 2o ) )
14	9 13	syl6ib	|- ( ( Fun A /\ ran A C_ { 1o , 2o } ) -> ( X e. dom A -> ( ( A ` X ) = 1o \/ ( A ` X ) = 2o ) ) )
15	4 5 14	syl2anc	|- ( A e. No -> ( X e. dom A -> ( ( A ` X ) = 1o \/ ( A ` X ) = 2o ) ) )
16	3 15	orim12d	|- ( A e. No -> ( ( -. X e. dom A \/ X e. dom A ) -> ( ( A ` X ) = (/) \/ ( ( A ` X ) = 1o \/ ( A ` X ) = 2o ) ) ) )
17	1 16	mpi	|- ( A e. No -> ( ( A ` X ) = (/) \/ ( ( A ` X ) = 1o \/ ( A ` X ) = 2o ) ) )
18		3orass	|- ( ( ( A ` X ) = (/) \/ ( A ` X ) = 1o \/ ( A ` X ) = 2o ) <-> ( ( A ` X ) = (/) \/ ( ( A ` X ) = 1o \/ ( A ` X ) = 2o ) ) )
19	17 18	sylibr	|- ( A e. No -> ( ( A ` X ) = (/) \/ ( A ` X ) = 1o \/ ( A ` X ) = 2o ) )