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 
|- ( A e. No -> ( -us " ( _Right ` A ) ) <

Proof

Step Hyp Ref Expression
1 negscut 
 |-  ( A e. No -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <
2 1 simp2d 
 |-  ( A e. No -> ( -us " ( _Right ` A ) ) <
3 1 simp3d 
 |-  ( A e. No -> { ( -us ` A ) } <
4 fvex 
 |-  ( -us ` A ) e. _V
5 4 snnz 
 |-  { ( -us ` A ) } =/= (/)
6 sslttr 
 |-  ( ( ( -us " ( _Right ` A ) ) < ( -us " ( _Right ` A ) ) <
7 5 6 mp3an3 
 |-  ( ( ( -us " ( _Right ` A ) ) < ( -us " ( _Right ` A ) ) <
8 2 3 7 syl2anc 
 |-  ( A e. No -> ( -us " ( _Right ` A ) ) <