Theorem negsf1o

Description: Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negsf1o	⊢ -us : No –1-1-onto→ No

Proof

Step	Hyp	Ref	Expression
1		negsf	⊢ -us : No ⟶ No
2		negs11	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ( -us ‘ 𝑥 ) = ( -us ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
3	2	biimpd	⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ( -us ‘ 𝑥 ) = ( -us ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
4	3	rgen2	⊢ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( -us ‘ 𝑥 ) = ( -us ‘ 𝑦 ) → 𝑥 = 𝑦 )
5		dff13	⊢ ( -us : No –1-1→ No ↔ ( -us : No ⟶ No ∧ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( -us ‘ 𝑥 ) = ( -us ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
6	1 4 5	mpbir2an	⊢ -us : No –1-1→ No
7		negsfo	⊢ -us : No –onto→ No
8		df-f1o	⊢ ( -us : No –1-1-onto→ No ↔ ( -us : No –1-1→ No ∧ -us : No –onto→ No ) )
9	6 7 8	mpbir2an	⊢ -us : No –1-1-onto→ No