Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-negs Structured version   Visualization version   GIF version

Definition df-negs 34047
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
StepHypRef Expression
1 cnegs 34044 . 2 class -us
2 vx . . . 4 setvar 𝑥
3 vn . . . 4 setvar 𝑛
4 cvv 3422 . . . 4 class V
53cv 1538 . . . . . 6 class 𝑛
62cv 1538 . . . . . . 7 class 𝑥
7 cright 33957 . . . . . . 7 class R
86, 7cfv 6418 . . . . . 6 class ( R ‘𝑥)
95, 8cima 5583 . . . . 5 class (𝑛 “ ( R ‘𝑥))
10 cleft 33956 . . . . . . 7 class L
116, 10cfv 6418 . . . . . 6 class ( L ‘𝑥)
125, 11cima 5583 . . . . 5 class (𝑛 “ ( L ‘𝑥))
13 cscut 33904 . . . . 5 class |s
149, 12, 13co 7255 . . . 4 class ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥)))
152, 3, 4, 4, 14cmpo 7257 . . 3 class (𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥))))
1615cnorec 34021 . 2 class norec ((𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥)))))
171, 16wceq 1539 1 wff -us = norec ((𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥)))))
Colors of variables: wff setvar class
This definition is referenced by:  negsfn  34049  negsval  34050
  Copyright terms: Public domain W3C validator