Theorem subsfo

Description: Surreal subtraction is an onto function. (Contributed by Scott Fenton, 17-May-2025)

	Ref	Expression
Assertion	subsfo	⊢ -s : ( No × No ) –onto→ No

Proof

Step	Hyp	Ref	Expression
1		subsf	⊢ -s : ( No × No ) ⟶ No
2		0no	⊢ 0s ∈ No
3		opelxpi	⊢ ( ( 𝑥 ∈ No ∧ 0s ∈ No ) → ⟨ 𝑥 , 0s ⟩ ∈ ( No × No ) )
4	2 3	mpan2	⊢ ( 𝑥 ∈ No → ⟨ 𝑥 , 0s ⟩ ∈ ( No × No ) )
5		subsval	⊢ ( ( 𝑥 ∈ No ∧ 0s ∈ No ) → ( 𝑥 -s 0s ) = ( 𝑥 +s ( -us ‘ 0s ) ) )
6	2 5	mpan2	⊢ ( 𝑥 ∈ No → ( 𝑥 -s 0s ) = ( 𝑥 +s ( -us ‘ 0s ) ) )
7		neg0s	⊢ ( -us ‘ 0s ) = 0s
8	7	oveq2i	⊢ ( 𝑥 +s ( -us ‘ 0s ) ) = ( 𝑥 +s 0s )
9		addsrid	⊢ ( 𝑥 ∈ No → ( 𝑥 +s 0s ) = 𝑥 )
10	8 9	eqtrid	⊢ ( 𝑥 ∈ No → ( 𝑥 +s ( -us ‘ 0s ) ) = 𝑥 )
11	6 10	eqtr2d	⊢ ( 𝑥 ∈ No → 𝑥 = ( 𝑥 -s 0s ) )
12		fveq2	⊢ ( 𝑦 = ⟨ 𝑥 , 0s ⟩ → ( -s ‘ 𝑦 ) = ( -s ‘ ⟨ 𝑥 , 0s ⟩ ) )
13		df-ov	⊢ ( 𝑥 -s 0s ) = ( -s ‘ ⟨ 𝑥 , 0s ⟩ )
14	12 13	eqtr4di	⊢ ( 𝑦 = ⟨ 𝑥 , 0s ⟩ → ( -s ‘ 𝑦 ) = ( 𝑥 -s 0s ) )
15	14	rspceeqv	⊢ ( ( ⟨ 𝑥 , 0s ⟩ ∈ ( No × No ) ∧ 𝑥 = ( 𝑥 -s 0s ) ) → ∃ 𝑦 ∈ ( No × No ) 𝑥 = ( -s ‘ 𝑦 ) )
16	4 11 15	syl2anc	⊢ ( 𝑥 ∈ No → ∃ 𝑦 ∈ ( No × No ) 𝑥 = ( -s ‘ 𝑦 ) )
17	16	rgen	⊢ ∀ 𝑥 ∈ No ∃ 𝑦 ∈ ( No × No ) 𝑥 = ( -s ‘ 𝑦 )
18		dffo3	⊢ ( -s : ( No × No ) –onto→ No ↔ ( -s : ( No × No ) ⟶ No ∧ ∀ 𝑥 ∈ No ∃ 𝑦 ∈ ( No × No ) 𝑥 = ( -s ‘ 𝑦 ) ) )
19	1 17 18	mpbir2an	⊢ -s : ( No × No ) –onto→ No