Definition df-negs

Description: Define surreal negation. Definition from Conway p. 5. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	df-negs	⊢ -us = norec ( ( 𝑥 ∈ V , 𝑛 ∈ V ↦ ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnegs	⊢ -us
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vn	⊢ 𝑛
4	3	cv	⊢ 𝑛
5		cright	⊢ R
6	1	cv	⊢ 𝑥
7	6 5	cfv	⊢ ( R ‘ 𝑥 )
8	4 7	cima	⊢ ( 𝑛 “ ( R ‘ 𝑥 ) )
9		ccuts	⊢ |s
10		cleft	⊢ L
11	6 10	cfv	⊢ ( L ‘ 𝑥 )
12	4 11	cima	⊢ ( 𝑛 “ ( L ‘ 𝑥 ) )
13	8 12 9	co	⊢ ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) )
14	1 3 2 2 13	cmpo	⊢ ( 𝑥 ∈ V , 𝑛 ∈ V ↦ ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) ) )
15	14	cnorec	⊢ norec ( ( 𝑥 ∈ V , 𝑛 ∈ V ↦ ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) ) ) )
16	0 15	wceq	⊢ -us = norec ( ( 𝑥 ∈ V , 𝑛 ∈ V ↦ ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) ) ) )