Theorem oldirr

Description: No surreal is a member of its birthday's old set. (Contributed by Scott Fenton, 10-Aug-2024)

	Ref	Expression
Assertion	oldirr	|- -. X e. ( _Old ` ( bday ` X ) )

Proof

Step	Hyp	Ref	Expression
1		bdayelon	|- ( bday ` X ) e. On
2	1	onirri	|- -. ( bday ` X ) e. ( bday ` X )
3		oldbdayim	|- ( ( ( bday ` X ) e. On /\ X e. ( _Old ` ( bday ` X ) ) ) -> ( bday ` X ) e. ( bday ` X ) )
4	1 3	mpan	|- ( X e. ( _Old ` ( bday ` X ) ) -> ( bday ` X ) e. ( bday ` X ) )
5	2 4	mto	|- -. X e. ( _Old ` ( bday ` X ) )