Metamath Proof Explorer


Theorem negscut2

Description: The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion negscut2 ANo+sRAs+sLA

Proof

Step Hyp Ref Expression
1 negscut ANo+sANo+sRAs+sA+sAs+sLA
2 1 simp2d ANo+sRAs+sA
3 1 simp3d ANo+sAs+sLA
4 fvex +sAV
5 4 snnz +sA
6 sslttr +sRAs+sA+sAs+sLA+sA+sRAs+sLA
7 5 6 mp3an3 +sRAs+sA+sAs+sLA+sRAs+sLA
8 2 3 7 syl2anc ANo+sRAs+sLA