Theorem negs0s

Description: Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	negs0s	⊢ ( -us ‘ 0s ) = 0s

Proof

Step	Hyp	Ref	Expression
1		right0s	⊢ ( R ‘ 0s ) = ∅
2	1	imaeq2i	⊢ ( -us “ ( R ‘ 0s ) ) = ( -us “ ∅ )
3		ima0	⊢ ( -us “ ∅ ) = ∅
4	2 3	eqtri	⊢ ( -us “ ( R ‘ 0s ) ) = ∅
5		left0s	⊢ ( L ‘ 0s ) = ∅
6	5	imaeq2i	⊢ ( -us “ ( L ‘ 0s ) ) = ( -us “ ∅ )
7	6 3	eqtri	⊢ ( -us “ ( L ‘ 0s ) ) = ∅
8	4 7	oveq12i	⊢ ( ( -us “ ( R ‘ 0s ) ) |s ( -us “ ( L ‘ 0s ) ) ) = ( ∅ |s ∅ )
9		0sno	⊢ 0s ∈ No
10		negsfv	⊢ ( 0s ∈ No → ( -us ‘ 0s ) = ( ( -us “ ( R ‘ 0s ) ) |s ( -us “ ( L ‘ 0s ) ) ) )
11	9 10	ax-mp	⊢ ( -us ‘ 0s ) = ( ( -us “ ( R ‘ 0s ) ) |s ( -us “ ( L ‘ 0s ) ) )
12		df-0s	⊢ 0s = ( ∅ |s ∅ )
13	8 11 12	3eqtr4i	⊢ ( -us ‘ 0s ) = 0s