Theorem old1

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

	Ref	Expression
Assertion	old1	Could not format assertion : No typesetting found for |- ( _Old ` 1o ) = { 0s } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
2		oldval	Could not format ( 1o e. On -> ( _Old ` 1o ) = U. ( _Made " 1o ) ) : No typesetting found for |- ( 1o e. On -> ( _Old ` 1o ) = U. ( _Made " 1o ) ) with typecode |-
3	1 2	ax-mp	Could not format ( _Old ` 1o ) = U. ( _Made " 1o ) : No typesetting found for |- ( _Old ` 1o ) = U. ( _Made " 1o ) with typecode |-
4		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
5	4	imaeq2i	Could not format ( _Made " 1o ) = ( _Made " { (/) } ) : No typesetting found for |- ( _Made " 1o ) = ( _Made " { (/) } ) with typecode |-
6		madef	Could not format _Made : On --> ~P No : No typesetting found for |- _Made : On --> ~P No with typecode |-
7		ffn	Could not format ( _Made : On --> ~P No -> _Made Fn On ) : No typesetting found for |- ( _Made : On --> ~P No -> _Made Fn On ) with typecode |-
8	6 7	ax-mp	Could not format _Made Fn On : No typesetting found for |- _Made Fn On with typecode |-
9		0elon	$$⊢\varnothing \in \mathrm{On}$$
10		fnsnfv	Could not format ( ( _Made Fn On /\ (/) e. On ) -> { ( _Made ` (/) ) } = ( _Made " { (/) } ) ) : No typesetting found for |- ( ( _Made Fn On /\ (/) e. On ) -> { ( _Made ` (/) ) } = ( _Made " { (/) } ) ) with typecode |-
11	8 9 10	mp2an	Could not format { ( _Made ` (/) ) } = ( _Made " { (/) } ) : No typesetting found for |- { ( _Made ` (/) ) } = ( _Made " { (/) } ) with typecode |-
12	5 11	eqtr4i	Could not format ( _Made " 1o ) = { ( _Made ` (/) ) } : No typesetting found for |- ( _Made " 1o ) = { ( _Made ` (/) ) } with typecode |-
13	12	unieqi	Could not format U. ( _Made " 1o ) = U. { ( _Made ` (/) ) } : No typesetting found for |- U. ( _Made " 1o ) = U. { ( _Made ` (/) ) } with typecode |-
14		fvex	Could not format ( _Made ` (/) ) e. _V : No typesetting found for |- ( _Made ` (/) ) e. _V with typecode |-
15	14	unisn	Could not format U. { ( _Made ` (/) ) } = ( _Made ` (/) ) : No typesetting found for |- U. { ( _Made ` (/) ) } = ( _Made ` (/) ) with typecode |-
16		made0	Could not format ( _Made ` (/) ) = { 0s } : No typesetting found for |- ( _Made ` (/) ) = { 0s } with typecode |-
17	15 16	eqtri	Could not format U. { ( _Made ` (/) ) } = { 0s } : No typesetting found for |- U. { ( _Made ` (/) ) } = { 0s } with typecode |-
18	13 17	eqtri	Could not format U. ( _Made " 1o ) = { 0s } : No typesetting found for |- U. ( _Made " 1o ) = { 0s } with typecode |-
19	3 18	eqtri	Could not format ( _Old ` 1o ) = { 0s } : No typesetting found for |- ( _Old ` 1o ) = { 0s } with typecode |-