Theorem znegscl

Description: The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Assertion	znegscl	⊢ ( 𝐴 ∈ ℤs → ( -us ‘ 𝐴 ) ∈ ℤs )

Proof

Step	Hyp	Ref	Expression
1		nnsno	⊢ ( 𝑛 ∈ ℕs → 𝑛 ∈ No )
2	1	adantr	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → 𝑛 ∈ No )
3		nnsno	⊢ ( 𝑚 ∈ ℕs → 𝑚 ∈ No )
4	3	adantl	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → 𝑚 ∈ No )
5	2 4	negsubsdi2d	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( -us ‘ ( 𝑛 -s 𝑚 ) ) = ( 𝑚 -s 𝑛 ) )
6		fveqeq2	⊢ ( 𝐴 = ( 𝑛 -s 𝑚 ) → ( ( -us ‘ 𝐴 ) = ( 𝑚 -s 𝑛 ) ↔ ( -us ‘ ( 𝑛 -s 𝑚 ) ) = ( 𝑚 -s 𝑛 ) ) )
7	5 6	syl5ibrcom	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( 𝐴 = ( 𝑛 -s 𝑚 ) → ( -us ‘ 𝐴 ) = ( 𝑚 -s 𝑛 ) ) )
8	7	reximdva	⊢ ( 𝑛 ∈ ℕs → ( ∃ 𝑚 ∈ ℕs 𝐴 = ( 𝑛 -s 𝑚 ) → ∃ 𝑚 ∈ ℕs ( -us ‘ 𝐴 ) = ( 𝑚 -s 𝑛 ) ) )
9	8	reximia	⊢ ( ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 𝐴 = ( 𝑛 -s 𝑚 ) → ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs ( -us ‘ 𝐴 ) = ( 𝑚 -s 𝑛 ) )
10		elzs	⊢ ( 𝐴 ∈ ℤs ↔ ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 𝐴 = ( 𝑛 -s 𝑚 ) )
11		elzs	⊢ ( ( -us ‘ 𝐴 ) ∈ ℤs ↔ ∃ 𝑚 ∈ ℕs ∃ 𝑛 ∈ ℕs ( -us ‘ 𝐴 ) = ( 𝑚 -s 𝑛 ) )
12		rexcom	⊢ ( ∃ 𝑚 ∈ ℕs ∃ 𝑛 ∈ ℕs ( -us ‘ 𝐴 ) = ( 𝑚 -s 𝑛 ) ↔ ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs ( -us ‘ 𝐴 ) = ( 𝑚 -s 𝑛 ) )
13	11 12	bitri	⊢ ( ( -us ‘ 𝐴 ) ∈ ℤs ↔ ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs ( -us ‘ 𝐴 ) = ( 𝑚 -s 𝑛 ) )
14	9 10 13	3imtr4i	⊢ ( 𝐴 ∈ ℤs → ( -us ‘ 𝐴 ) ∈ ℤs )