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	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ‘ 𝑋 ) = ∅ ∨ ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) )

Proof

Step	Hyp	Ref	Expression
1		pm2.1	⊢ ( ¬ 𝑋 ∈ dom 𝐴 ∨ 𝑋 ∈ dom 𝐴 )
2		ndmfv	⊢ ( ¬ 𝑋 ∈ dom 𝐴 → ( 𝐴 ‘ 𝑋 ) = ∅ )
3	2	a1i	⊢ ( 𝐴 ∈ No → ( ¬ 𝑋 ∈ dom 𝐴 → ( 𝐴 ‘ 𝑋 ) = ∅ ) )
4		nofun	⊢ ( 𝐴 ∈ No → Fun 𝐴 )
5		norn	⊢ ( 𝐴 ∈ No → ran 𝐴 ⊆ { 1o , 2o } )
6		fvelrn	⊢ ( ( Fun 𝐴 ∧ 𝑋 ∈ dom 𝐴 ) → ( 𝐴 ‘ 𝑋 ) ∈ ran 𝐴 )
7		ssel	⊢ ( ran 𝐴 ⊆ { 1o , 2o } → ( ( 𝐴 ‘ 𝑋 ) ∈ ran 𝐴 → ( 𝐴 ‘ 𝑋 ) ∈ { 1o , 2o } ) )
8	6 7	syl5com	⊢ ( ( Fun 𝐴 ∧ 𝑋 ∈ dom 𝐴 ) → ( ran 𝐴 ⊆ { 1o , 2o } → ( 𝐴 ‘ 𝑋 ) ∈ { 1o , 2o } ) )
9	8	impancom	⊢ ( ( Fun 𝐴 ∧ ran 𝐴 ⊆ { 1o , 2o } ) → ( 𝑋 ∈ dom 𝐴 → ( 𝐴 ‘ 𝑋 ) ∈ { 1o , 2o } ) )
10		1oex	⊢ 1o ∈ V
11		2on	⊢ 2o ∈ On
12	11	elexi	⊢ 2o ∈ V
13	10 12	elpr2	⊢ ( ( 𝐴 ‘ 𝑋 ) ∈ { 1o , 2o } ↔ ( ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) )
14	9 13	imbitrdi	⊢ ( ( Fun 𝐴 ∧ ran 𝐴 ⊆ { 1o , 2o } ) → ( 𝑋 ∈ dom 𝐴 → ( ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) ) )
15	4 5 14	syl2anc	⊢ ( 𝐴 ∈ No → ( 𝑋 ∈ dom 𝐴 → ( ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) ) )
16	3 15	orim12d	⊢ ( 𝐴 ∈ No → ( ( ¬ 𝑋 ∈ dom 𝐴 ∨ 𝑋 ∈ dom 𝐴 ) → ( ( 𝐴 ‘ 𝑋 ) = ∅ ∨ ( ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) ) ) )
17	1 16	mpi	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ‘ 𝑋 ) = ∅ ∨ ( ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) ) )
18		3orass	⊢ ( ( ( 𝐴 ‘ 𝑋 ) = ∅ ∨ ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) ↔ ( ( 𝐴 ‘ 𝑋 ) = ∅ ∨ ( ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) ) )
19	17 18	sylibr	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ‘ 𝑋 ) = ∅ ∨ ( 𝐴 ‘ 𝑋 ) = 1o ∨ ( 𝐴 ‘ 𝑋 ) = 2o ) )