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	⊢ ¬ 𝑋 ∈ ( O ‘ ( bday ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		bdayelon	⊢ ( bday ‘ 𝑋 ) ∈ On
2	1	onirri	⊢ ¬ ( bday ‘ 𝑋 ) ∈ ( bday ‘ 𝑋 )
3		oldbdayim	⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ 𝑋 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ) → ( bday ‘ 𝑋 ) ∈ ( bday ‘ 𝑋 ) )
4	1 3	mpan	⊢ ( 𝑋 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → ( bday ‘ 𝑋 ) ∈ ( bday ‘ 𝑋 ) )
5	2 4	mto	⊢ ¬ 𝑋 ∈ ( O ‘ ( bday ‘ 𝑋 ) )