df-negs

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

		Ref	Expression
	Assertion	df-negs	$⊢ +_{s} = {norec}_{s} #A# ((x \in V, n \in V ⟼ n [R (x)] \|_{s} n [L (x)]))$

Step	Hyp	Ref	Expression
0		cnegs	$class +_{s}$
1		vx	$setvar x$
2		cvv	$class V$
3		vn	$setvar n$
4	3	cv	$setvar n$
5		cright	$class R$
6	1	cv	$setvar x$
7	6 5	cfv	$class R (x)$
8	4 7	cima	$class n [R (x)]$
9		cscut	$class \|_{s}$
10		cleft	$class L$
11	6 10	cfv	$class L (x)$
12	4 11	cima	$class n [L (x)]$
13	8 12 9	co	$class (n [R (x)] \|_{s} n [L (x)])$
14	1 3 2 2 13	cmpo	$class (x \in V, n \in V ⟼ n [R (x)] \|_{s} n [L (x)])$
15	14	cnorec	$class {norec}_{s} #A# ((x \in V, n \in V ⟼ n [R (x)] \|_{s} n [L (x)]))$
16	0 15	wceq	$wff +_{s} = {norec}_{s} #A# ((x \in V, n \in V ⟼ n [R (x)] \|_{s} n [L (x)]))$

Metamath Proof Explorer