Theorem old0

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

	Ref	Expression
Assertion	old0	⊢ ( O ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		0elon	⊢ ∅ ∈ On
2		oldval	⊢ ( ∅ ∈ On → ( O ‘ ∅ ) = ∪ ( M “ ∅ ) )
3	1 2	ax-mp	⊢ ( O ‘ ∅ ) = ∪ ( M “ ∅ )
4		ima0	⊢ ( M “ ∅ ) = ∅
5	4	unieqi	⊢ ∪ ( M “ ∅ ) = ∪ ∅
6		uni0	⊢ ∪ ∅ = ∅
7	3 5 6	3eqtri	⊢ ( O ‘ ∅ ) = ∅