Theorem bdayval

Description: The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011)

	Ref	Expression
Assertion	bdayval	⊢ ( 𝐴 ∈ No → ( bday ‘ 𝐴 ) = dom 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dmexg	⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ V )
2		dmeq	⊢ ( 𝑥 = 𝐴 → dom 𝑥 = dom 𝐴 )
3		df-bday	⊢ bday = ( 𝑥 ∈ No ↦ dom 𝑥 )
4	2 3	fvmptg	⊢ ( ( 𝐴 ∈ No ∧ dom 𝐴 ∈ V ) → ( bday ‘ 𝐴 ) = dom 𝐴 )
5	1 4	mpdan	⊢ ( 𝐴 ∈ No → ( bday ‘ 𝐴 ) = dom 𝐴 )