Metamath Proof Explorer


Theorem old0

Description: No surreal is older than (/) . (Contributed by Scott Fenton, 7-Aug-2024)

Ref Expression
Assertion old0 Old =

Proof

Step Hyp Ref Expression
1 0elon On
2 oldval On Old = M
3 1 2 ax-mp Old = M
4 ima0 M =
5 4 unieqi M =
6 uni0 =
7 3 5 6 3eqtri Old =