Metamath Proof Explorer

Theorem scutfo

Description: The surreal cut function is onto. (Contributed by Scott Fenton, 23-Aug-2024)

Ref Expression
Assertion scutfo 
|- |s : < No

Proof

Step Hyp Ref Expression
1 scutf 
 |-  |s : < No
2 lltropt 
 |-  ( x e. No -> ( _L ` x ) <
3 df-br 
 |-  ( ( _L ` x ) < <. ( _L ` x ) , ( _R ` x ) >. e. <
4 2 3 sylib 
 |-  ( x e. No -> <. ( _L ` x ) , ( _R ` x ) >. e. <
5 lrcut 
 |-  ( x e. No -> ( ( _L ` x ) |s ( _R ` x ) ) = x )
6 5 eqcomd 
 |-  ( x e. No -> x = ( ( _L ` x ) |s ( _R ` x ) ) )
7 fveq2 
 |-  ( y = <. ( _L ` x ) , ( _R ` x ) >. -> ( |s ` y ) = ( |s ` <. ( _L ` x ) , ( _R ` x ) >. ) )
8 df-ov 
 |-  ( ( _L ` x ) |s ( _R ` x ) ) = ( |s ` <. ( _L ` x ) , ( _R ` x ) >. )
9 7 8 eqtr4di 
 |-  ( y = <. ( _L ` x ) , ( _R ` x ) >. -> ( |s ` y ) = ( ( _L ` x ) |s ( _R ` x ) ) )
10 9 rspceeqv 
 |-  ( ( <. ( _L ` x ) , ( _R ` x ) >. e. < E. y e. <
11 4 6 10 syl2anc 
 |-  ( x e. No -> E. y e. <
12 11 rgen 
 |-  A. x e. No E. y e. <
13 dffo3 
 |-  ( |s : < No <-> ( |s : < No /\ A. x e. No E. y e. <
14 1 12 13 mpbir2an 
 |-  |s : < No