Theorem nofun

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

	Ref	Expression
Assertion	nofun	⊢ ( 𝐴 ∈ No → Fun 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elno	⊢ ( 𝐴 ∈ No ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } )
2		ffun	⊢ ( 𝐴 : 𝑥 ⟶ { 1o , 2o } → Fun 𝐴 )
3	2	rexlimivw	⊢ ( ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } → Fun 𝐴 )
4	1 3	sylbi	⊢ ( 𝐴 ∈ No → Fun 𝐴 )