Theorem negscut2

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

	Ref	Expression
Assertion	negscut2	Could not format assertion : No typesetting found for |- ( A e. No -> ( -us " ( _Right ` A ) ) <

Proof

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