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 e. No
2		negsval	|- ( 1s e. No -> ( -us ` 1s ) = ( ( -us " ( _Right ` 1s ) ) |s ( -us " ( _Left ` 1s ) ) ) )
3	1 2	ax-mp	|- ( -us ` 1s ) = ( ( -us " ( _Right ` 1s ) ) |s ( -us " ( _Left ` 1s ) ) )
4		right1s	|- ( _Right ` 1s ) = (/)
5	4	imaeq2i	|- ( -us " ( _Right ` 1s ) ) = ( -us " (/) )
6		ima0	|- ( -us " (/) ) = (/)
7	5 6	eqtri	|- ( -us " ( _Right ` 1s ) ) = (/)
8		left1s	|- ( _Left ` 1s ) = { 0s }
9	8	imaeq2i	|- ( -us " ( _Left ` 1s ) ) = ( -us " { 0s } )
10		negsfn	|- -us Fn No
11		0sno	|- 0s e. No
12		fnimapr	|- ( ( -us Fn No /\ 0s e. No /\ 0s e. 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 " ( _Left ` 1s ) ) = { 0s }
21	7 20	oveq12i	|- ( ( -us " ( _Right ` 1s ) ) |s ( -us " ( _Left ` 1s ) ) ) = ( (/) |s { 0s } )
22	3 21	eqtri	|- ( -us ` 1s ) = ( (/) |s { 0s } )