Metamath Proof Explorer


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 Old bday X

Proof

Step Hyp Ref Expression
1 bdayelon bday X On
2 1 onirri ¬ bday X bday X
3 oldbdayim X Old bday X bday X bday X
4 2 3 mto ¬ X Old bday X