Theorem scutfo

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

	Ref	Expression
Assertion	scutfo	⊢ |s : <<s –onto→ No

Proof

Step	Hyp	Ref	Expression
1		scutf	⊢ |s : <<s ⟶ No
2		lltropt	⊢ ( 𝑥 ∈ No → ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 ) )
3		df-br	⊢ ( ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 ) ↔ ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ ∈ <<s )
4	2 3	sylib	⊢ ( 𝑥 ∈ No → ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ ∈ <<s )
5		lrcut	⊢ ( 𝑥 ∈ No → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) = 𝑥 )
6	5	eqcomd	⊢ ( 𝑥 ∈ No → 𝑥 = ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) )
7		fveq2	⊢ ( 𝑦 = ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ → ( |s ‘ 𝑦 ) = ( |s ‘ ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ ) )
8		df-ov	⊢ ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) = ( |s ‘ ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ )
9	7 8	eqtr4di	⊢ ( 𝑦 = ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ → ( |s ‘ 𝑦 ) = ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) )
10	9	rspceeqv	⊢ ( ( ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ ∈ <<s ∧ 𝑥 = ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) ) → ∃ 𝑦 ∈ <<s 𝑥 = ( |s ‘ 𝑦 ) )
11	4 6 10	syl2anc	⊢ ( 𝑥 ∈ No → ∃ 𝑦 ∈ <<s 𝑥 = ( |s ‘ 𝑦 ) )
12	11	rgen	⊢ ∀ 𝑥 ∈ No ∃ 𝑦 ∈ <<s 𝑥 = ( |s ‘ 𝑦 )
13		dffo3	⊢ ( |s : <<s –onto→ No ↔ ( |s : <<s ⟶ No ∧ ∀ 𝑥 ∈ No ∃ 𝑦 ∈ <<s 𝑥 = ( |s ‘ 𝑦 ) ) )
14	1 12 13	mpbir2an	⊢ |s : <<s –onto→ No