Definition df-negs 34120

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

Assertion

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

Distinct variable group:   𝑥,𝑛

Detailed syntax breakdown of Definition df-negs

Step	Hyp	Ref	Expression
1		cnegs 34117	. 2 class -us
2		vx	. . . 4 setvar 𝑥
3		vn	. . . 4 setvar 𝑛
4		cvv 3432	. . . 4 class V
5	3	cv 1538	. . . . . 6 class 𝑛
6	2	cv 1538	. . . . . . 7 class 𝑥
7		cright 34030	. . . . . . 7 class R
8	6, 7	cfv 6433	. . . . . 6 class ( R ‘𝑥)
9	5, 8	cima 5592	. . . . 5 class (𝑛 “ ( R ‘𝑥))
10		cleft 34029	. . . . . . 7 class L
11	6, 10	cfv 6433	. . . . . 6 class ( L ‘𝑥)
12	5, 11	cima 5592	. . . . 5 class (𝑛 “ ( L ‘𝑥))
13		cscut 33977	. . . . 5 class |s
14	9, 12, 13	co 7275	. . . 4 class ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥)))
15	2, 3, 4, 4, 14	cmpo 7277	. . 3 class (𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥))))
16	15	cnorec 34094	. 2 class norec ((𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥)))))
17	1, 16	wceq 1539	1 wff -us = norec ((𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥)))))

This definition is referenced by:  negsfn  34122  negsval  34123