Metamath Proof Explorer


Theorem newbday

Description: A surreal is an element of a new set iff its birthday is equal to that ordinal. Remark in Conway p. 29. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion newbday A On X No X N A bday X = A

Proof

Step Hyp Ref Expression
1 madebday A On X No X M A bday X A
2 oldbday A On X No X Old A bday X A
3 2 notbid A On X No ¬ X Old A ¬ bday X A
4 1 3 anbi12d A On X No X M A ¬ X Old A bday X A ¬ bday X A
5 newval N A = M A Old A
6 5 a1i A On N A = M A Old A
7 6 eleq2d A On X N A X M A Old A
8 eldif X M A Old A X M A ¬ X Old A
9 7 8 bitrdi A On X N A X M A ¬ X Old A
10 9 adantr A On X No X N A X M A ¬ X Old A
11 bdayelon bday X On
12 11 onordi Ord bday X
13 eloni A On Ord A
14 ordtri4 Ord bday X Ord A bday X = A bday X A ¬ bday X A
15 12 13 14 sylancr A On bday X = A bday X A ¬ bday X A
16 15 adantr A On X No bday X = A bday X A ¬ bday X A
17 4 10 16 3bitr4d A On X No X N A bday X = A