Description: The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | negscut2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negscut | |
|
2 | 1 | simp2d | |
3 | 1 | simp3d | |
4 | fvex | |
|
5 | 4 | snnz | |
6 | sslttr | |
|
7 | 5 6 | mp3an3 | |
8 | 2 3 7 | syl2anc | |