Theorem old1

Description: The only surreal older than 1o is 0s . (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	old1	|- ( _Old ` 1o ) = { 0s }

Proof

Step	Hyp	Ref	Expression
1		1on	|- 1o e. On
2		oldval	|- ( 1o e. On -> ( _Old ` 1o ) = U. ( _Made " 1o ) )
3	1 2	ax-mp	|- ( _Old ` 1o ) = U. ( _Made " 1o )
4		df1o2	|- 1o = { (/) }
5	4	imaeq2i	|- ( _Made " 1o ) = ( _Made " { (/) } )
6		madef	|- _Made : On --> ~P No
7		ffn	|- ( _Made : On --> ~P No -> _Made Fn On )
8	6 7	ax-mp	|- _Made Fn On
9		0elon	|- (/) e. On
10		fnsnfv	|- ( ( _Made Fn On /\ (/) e. On ) -> { ( _Made ` (/) ) } = ( _Made " { (/) } ) )
11	8 9 10	mp2an	|- { ( _Made ` (/) ) } = ( _Made " { (/) } )
12	5 11	eqtr4i	|- ( _Made " 1o ) = { ( _Made ` (/) ) }
13	12	unieqi	|- U. ( _Made " 1o ) = U. { ( _Made ` (/) ) }
14		fvex	|- ( _Made ` (/) ) e. _V
15	14	unisn	|- U. { ( _Made ` (/) ) } = ( _Made ` (/) )
16		made0	|- ( _Made ` (/) ) = { 0s }
17	15 16	eqtri	|- U. { ( _Made ` (/) ) } = { 0s }
18	13 17	eqtri	|- U. ( _Made " 1o ) = { 0s }
19	3 18	eqtri	|- ( _Old ` 1o ) = { 0s }