Theorem cutsfo

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

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

Proof

Step	Hyp	Ref	Expression
1		cutsf	$$⊢{|}_s:{\ll }_s⟶\mathrm{No}$$
2		lltr	$$⊢L\left(x\right){\ll }_{s}R\left(x\right)$$
3		df-br	$$⊢L\left(x\right){\ll }_{s}R\left(x\right)\leftrightarrow ⟨L\left(x\right),R\left(x\right)⟩\in {\ll }_s$$
4	2 3	mpbi	$$⊢⟨L\left(x\right),R\left(x\right)⟩\in {\ll }_s$$
5		lrcut	$$⊢x\in \mathrm{No}\to L\left(x\right){|}_{s}R\left(x\right)=x$$
6	5	eqcomd	$$⊢x\in \mathrm{No}\to x=L\left(x\right){|}_{s}R\left(x\right)$$
7		fveq2	$$⊢y=⟨L\left(x\right),R\left(x\right)⟩\to {|}_s\left(y\right)={|}_s\left(⟨L\left(x\right),R\left(x\right)⟩\right)$$
8		df-ov	$$⊢L\left(x\right){|}_{s}R\left(x\right)={|}_s\left(⟨L\left(x\right),R\left(x\right)⟩\right)$$
9	7 8	eqtr4di	$$⊢y=⟨L\left(x\right),R\left(x\right)⟩\to {|}_s\left(y\right)=L\left(x\right){|}_{s}R\left(x\right)$$
10	9	rspceeqv	$$⊢\left(⟨L\left(x\right),R\left(x\right)⟩\in {\ll }_s\wedge x=L\left(x\right){|}_{s}R\left(x\right)\right)\to \exists y\in {\ll }_{s}x={|}_s\left(y\right)$$
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}$$