Theorem fvnobday

Description: The value of a surreal at its birthday is (/) . (Contributed by Scott Fenton, 14-Jun-2011) (Proof shortened by SF, 14-Apr-2012)

	Ref	Expression
Assertion	fvnobday	⊢ ( 𝐴 ∈ No → ( 𝐴 ‘ ( bday ‘ 𝐴 ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		bdayval	⊢ ( 𝐴 ∈ No → ( bday ‘ 𝐴 ) = dom 𝐴 )
2		nodmord	⊢ ( 𝐴 ∈ No → Ord dom 𝐴 )
3		ordirr	⊢ ( Ord dom 𝐴 → ¬ dom 𝐴 ∈ dom 𝐴 )
4	2 3	syl	⊢ ( 𝐴 ∈ No → ¬ dom 𝐴 ∈ dom 𝐴 )
5	1 4	eqneltrd	⊢ ( 𝐴 ∈ No → ¬ ( bday ‘ 𝐴 ) ∈ dom 𝐴 )
6		ndmfv	⊢ ( ¬ ( bday ‘ 𝐴 ) ∈ dom 𝐴 → ( 𝐴 ‘ ( bday ‘ 𝐴 ) ) = ∅ )
7	5 6	syl	⊢ ( 𝐴 ∈ No → ( 𝐴 ‘ ( bday ‘ 𝐴 ) ) = ∅ )