Theorem negs1s

Description: An expression for negative surreal one. (Contributed by Scott Fenton, 24-Jul-2025)

	Ref	Expression
Assertion	negs1s	⊢ ( -us ‘ 1s ) = ( ∅ |s { 0s } )

Proof

Step	Hyp	Ref	Expression
1		1sno	⊢ 1s ∈ No
2		negsval	⊢ ( 1s ∈ No → ( -us ‘ 1s ) = ( ( -us “ ( R ‘ 1s ) ) |s ( -us “ ( L ‘ 1s ) ) ) )
3	1 2	ax-mp	⊢ ( -us ‘ 1s ) = ( ( -us “ ( R ‘ 1s ) ) |s ( -us “ ( L ‘ 1s ) ) )
4		right1s	⊢ ( R ‘ 1s ) = ∅
5	4	imaeq2i	⊢ ( -us “ ( R ‘ 1s ) ) = ( -us “ ∅ )
6		ima0	⊢ ( -us “ ∅ ) = ∅
7	5 6	eqtri	⊢ ( -us “ ( R ‘ 1s ) ) = ∅
8		left1s	⊢ ( L ‘ 1s ) = { 0s }
9	8	imaeq2i	⊢ ( -us “ ( L ‘ 1s ) ) = ( -us “ { 0s } )
10		negsfn	⊢ -us Fn No
11		0sno	⊢ 0s ∈ No
12		fnimapr	⊢ ( ( -us Fn No ∧ 0s ∈ No ∧ 0s ∈ No ) → ( -us “ { 0s , 0s } ) = { ( -us ‘ 0s ) , ( -us ‘ 0s ) } )
13	10 11 11 12	mp3an	⊢ ( -us “ { 0s , 0s } ) = { ( -us ‘ 0s ) , ( -us ‘ 0s ) }
14		negs0s	⊢ ( -us ‘ 0s ) = 0s
15	14 14	preq12i	⊢ { ( -us ‘ 0s ) , ( -us ‘ 0s ) } = { 0s , 0s }
16	13 15	eqtri	⊢ ( -us “ { 0s , 0s } ) = { 0s , 0s }
17		dfsn2	⊢ { 0s } = { 0s , 0s }
18	17	imaeq2i	⊢ ( -us “ { 0s } ) = ( -us “ { 0s , 0s } )
19	16 18 17	3eqtr4i	⊢ ( -us “ { 0s } ) = { 0s }
20	9 19	eqtri	⊢ ( -us “ ( L ‘ 1s ) ) = { 0s }
21	7 20	oveq12i	⊢ ( ( -us “ ( R ‘ 1s ) ) |s ( -us “ ( L ‘ 1s ) ) ) = ( ∅ |s { 0s } )
22	3 21	eqtri	⊢ ( -us ‘ 1s ) = ( ∅ |s { 0s } )