Theorem nofnbday

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

	Ref	Expression
Assertion	nofnbday	$$⊢A\in \mathrm{No}\to AFn\mathrm{bday}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nofun	$$⊢A\in \mathrm{No}\to \mathrm{Fun}A$$
2		bdayval	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left(A\right)=\mathrm{dom}A$$
3	2	eqcomd	$$⊢A\in \mathrm{No}\to \mathrm{dom}A=\mathrm{bday}\left(A\right)$$
4		df-fn	$$⊢AFn\mathrm{bday}\left(A\right)\leftrightarrow \left(\mathrm{Fun}A\wedge \mathrm{dom}A=\mathrm{bday}\left(A\right)\right)$$
5	1 3 4	sylanbrc	$$⊢A\in \mathrm{No}\to AFn\mathrm{bday}\left(A\right)$$