Metamath Proof Explorer


Theorem negsf

Description: Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion negsf + s : No No

Proof

Step Hyp Ref Expression
1 negsfn + s Fn No
2 negscl x No + s x No
3 2 rgen x No + s x No
4 ffnfv + s : No No + s Fn No x No + s x No
5 1 3 4 mpbir2an + s : No No