Theorem addsfo

Description: Surreal addition is onto. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Assertion	addsfo	⊢ +s : ( No × No ) –onto→ No

Proof

Step	Hyp	Ref	Expression
1		addsf	⊢ +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		addsrid	⊢ ( 𝑧 ∈ No → ( 𝑧 +s 0s ) = 𝑧 )
6	5	eqcomd	⊢ ( 𝑧 ∈ No → 𝑧 = ( 𝑧 +s 0s ) )
7		fveq2	⊢ ( 𝑥 = ⟨ 𝑧 , 0s ⟩ → ( +s ‘ 𝑥 ) = ( +s ‘ ⟨ 𝑧 , 0s ⟩ ) )
8		df-ov	⊢ ( 𝑧 +s 0s ) = ( +s ‘ ⟨ 𝑧 , 0s ⟩ )
9	7 8	eqtr4di	⊢ ( 𝑥 = ⟨ 𝑧 , 0s ⟩ → ( +s ‘ 𝑥 ) = ( 𝑧 +s 0s ) )
10	9	rspceeqv	⊢ ( ( ⟨ 𝑧 , 0s ⟩ ∈ ( No × No ) ∧ 𝑧 = ( 𝑧 +s 0s ) ) → ∃ 𝑥 ∈ ( No × No ) 𝑧 = ( +s ‘ 𝑥 ) )
11	4 6 10	syl2anc	⊢ ( 𝑧 ∈ No → ∃ 𝑥 ∈ ( No × No ) 𝑧 = ( +s ‘ 𝑥 ) )
12	11	rgen	⊢ ∀ 𝑧 ∈ No ∃ 𝑥 ∈ ( No × No ) 𝑧 = ( +s ‘ 𝑥 )
13		dffo3	⊢ ( +s : ( No × No ) –onto→ No ↔ ( +s : ( No × No ) ⟶ No ∧ ∀ 𝑧 ∈ No ∃ 𝑥 ∈ ( No × No ) 𝑧 = ( +s ‘ 𝑥 ) ) )
14	1 12 13	mpbir2an	⊢ +s : ( No × No ) –onto→ No