Theorem old1

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

	Ref	Expression
Assertion	old1	⊢ ( O ‘ 1o ) = { 0s }

Proof

Step	Hyp	Ref	Expression
1		1on	⊢ 1o ∈ On
2		oldval	⊢ ( 1o ∈ On → ( O ‘ 1o ) = ∪ ( M “ 1o ) )
3	1 2	ax-mp	⊢ ( O ‘ 1o ) = ∪ ( M “ 1o )
4		df1o2	⊢ 1o = { ∅ }
5	4	imaeq2i	⊢ ( M “ 1o ) = ( M “ { ∅ } )
6		madef	⊢ M : On ⟶ 𝒫 No
7		ffn	⊢ ( M : On ⟶ 𝒫 No → M Fn On )
8	6 7	ax-mp	⊢ M Fn On
9		0elon	⊢ ∅ ∈ On
10		fnsnfv	⊢ ( ( M Fn On ∧ ∅ ∈ On ) → { ( M ‘ ∅ ) } = ( M “ { ∅ } ) )
11	8 9 10	mp2an	⊢ { ( M ‘ ∅ ) } = ( M “ { ∅ } )
12	5 11	eqtr4i	⊢ ( M “ 1o ) = { ( M ‘ ∅ ) }
13	12	unieqi	⊢ ∪ ( M “ 1o ) = ∪ { ( M ‘ ∅ ) }
14		fvex	⊢ ( M ‘ ∅ ) ∈ V
15	14	unisn	⊢ ∪ { ( M ‘ ∅ ) } = ( M ‘ ∅ )
16		made0	⊢ ( M ‘ ∅ ) = { 0s }
17	15 16	eqtri	⊢ ∪ { ( M ‘ ∅ ) } = { 0s }
18	13 17	eqtri	⊢ ∪ ( M “ 1o ) = { 0s }
19	3 18	eqtri	⊢ ( O ‘ 1o ) = { 0s }