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 
 |-  (/) e. On
2 oldval 
 |-  ( (/) e. On -> ( _Old ` (/) ) = U. ( _M " (/) ) )
3 1 2 ax-mp 
 |-  ( _Old ` (/) ) = U. ( _M " (/) )
4 ima0 
 |-  ( _M " (/) ) = (/)
5 4 unieqi 
 |-  U. ( _M " (/) ) = U. (/)
6 uni0 
 |-  U. (/) = (/)
7 3 5 6 3eqtri 
 |-  ( _Old ` (/) ) = (/)