Theorem scutfo

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

	Ref	Expression
Assertion	scutfo	$$⊢{|}_s:{\ll }_s\underset{onto}{⟶}\mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		scutf	$$⊢{|}_s:{\ll }_s⟶\mathrm{No}$$
2		lltropt	Could not format ( _Left ` x ) <
3		df-br	Could not format ( ( _Left ` x ) < <. ( _Left ` x ) , ( _Right ` x ) >. e. < <. ( _Left ` x ) , ( _Right ` x ) >. e. <
4	2 3	mpbi	Could not format <. ( _Left ` x ) , ( _Right ` x ) >. e. <. e. <
5		lrcut	Could not format ( x e. No -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x ) : No typesetting found for |- ( x e. No -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x ) with typecode |-
6	5	eqcomd	Could not format ( x e. No -> x = ( ( _Left ` x ) |s ( _Right ` x ) ) ) : No typesetting found for |- ( x e. No -> x = ( ( _Left ` x ) |s ( _Right ` x ) ) ) with typecode |-
7		fveq2	Could not format ( y = <. ( _Left ` x ) , ( _Right ` x ) >. -> ( |s ` y ) = ( |s ` <. ( _Left ` x ) , ( _Right ` x ) >. ) ) : No typesetting found for |- ( y = <. ( _Left ` x ) , ( _Right ` x ) >. -> ( |s ` y ) = ( |s ` <. ( _Left ` x ) , ( _Right ` x ) >. ) ) with typecode |-
8		df-ov	Could not format ( ( _Left ` x ) |s ( _Right ` x ) ) = ( |s ` <. ( _Left ` x ) , ( _Right ` x ) >. ) : No typesetting found for |- ( ( _Left ` x ) |s ( _Right ` x ) ) = ( |s ` <. ( _Left ` x ) , ( _Right ` x ) >. ) with typecode |-
9	7 8	eqtr4di	Could not format ( y = <. ( _Left ` x ) , ( _Right ` x ) >. -> ( |s ` y ) = ( ( _Left ` x ) |s ( _Right ` x ) ) ) : No typesetting found for |- ( y = <. ( _Left ` x ) , ( _Right ` x ) >. -> ( |s ` y ) = ( ( _Left ` x ) |s ( _Right ` x ) ) ) with typecode |-
10	9	rspceeqv	Could not format ( ( <. ( _Left ` x ) , ( _Right ` x ) >. e. < E. y e. <. e. < E. y e. <
11	4 6 10	sylancr	$$⊢x\in \mathrm{No}\to \exists y\in {\ll }_{s}x={|}_s\left(y\right)$$
12	11	rgen	$$⊢\forall x\in \mathrm{No}\exists y\in {\ll }_{s}x={|}_s\left(y\right)$$
13		dffo3	$$⊢{|}_s:{\ll }_s\underset{onto}{⟶}\mathrm{No}\leftrightarrow \left({|}_s:{\ll }_s⟶\mathrm{No}\wedge \forall x\in \mathrm{No}\exists y\in {\ll }_{s}x={|}_s\left(y\right)\right)$$
14	1 12 13	mpbir2an	$$⊢{|}_s:{\ll }_s\underset{onto}{⟶}\mathrm{No}$$