Theorem nofnbday

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

	Ref	Expression
Assertion	nofnbday	⊢ ( 𝐴 ∈ No → 𝐴 Fn ( bday ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nofun	⊢ ( 𝐴 ∈ No → Fun 𝐴 )
2		bdayval	⊢ ( 𝐴 ∈ No → ( bday ‘ 𝐴 ) = dom 𝐴 )
3	2	eqcomd	⊢ ( 𝐴 ∈ No → dom 𝐴 = ( bday ‘ 𝐴 ) )
4		df-fn	⊢ ( 𝐴 Fn ( bday ‘ 𝐴 ) ↔ ( Fun 𝐴 ∧ dom 𝐴 = ( bday ‘ 𝐴 ) ) )
5	1 3 4	sylanbrc	⊢ ( 𝐴 ∈ No → 𝐴 Fn ( bday ‘ 𝐴 ) )