Theorem zcuts0

Description: Either the left or right set of a surreal integer is empty. (Contributed by Scott Fenton, 21-Feb-2026)

	Ref	Expression
Assertion	zcuts0	⊢ ( 𝐴 ∈ ℤs → ( ( L ‘ 𝐴 ) = ∅ ∨ ( R ‘ 𝐴 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		elzn0s	⊢ ( 𝐴 ∈ ℤs ↔ ( 𝐴 ∈ No ∧ ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ) )
2		n0on	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ Ons )
3		elons	⊢ ( 𝐴 ∈ Ons ↔ ( 𝐴 ∈ No ∧ ( R ‘ 𝐴 ) = ∅ ) )
4	3	simprbi	⊢ ( 𝐴 ∈ Ons → ( R ‘ 𝐴 ) = ∅ )
5	2 4	syl	⊢ ( 𝐴 ∈ ℕ0s → ( R ‘ 𝐴 ) = ∅ )
6	5	a1i	⊢ ( 𝐴 ∈ No → ( 𝐴 ∈ ℕ0s → ( R ‘ 𝐴 ) = ∅ ) )
7		simpl	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → 𝐴 ∈ No )
8	7	negscld	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( -us ‘ 𝐴 ) ∈ No )
9		negleft	⊢ ( ( -us ‘ 𝐴 ) ∈ No → ( L ‘ ( -us ‘ ( -us ‘ 𝐴 ) ) ) = ( -us “ ( R ‘ ( -us ‘ 𝐴 ) ) ) )
10	8 9	syl	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( L ‘ ( -us ‘ ( -us ‘ 𝐴 ) ) ) = ( -us “ ( R ‘ ( -us ‘ 𝐴 ) ) ) )
11		negnegs	⊢ ( 𝐴 ∈ No → ( -us ‘ ( -us ‘ 𝐴 ) ) = 𝐴 )
12	11	fveq2d	⊢ ( 𝐴 ∈ No → ( L ‘ ( -us ‘ ( -us ‘ 𝐴 ) ) ) = ( L ‘ 𝐴 ) )
13	12	adantr	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( L ‘ ( -us ‘ ( -us ‘ 𝐴 ) ) ) = ( L ‘ 𝐴 ) )
14		n0on	⊢ ( ( -us ‘ 𝐴 ) ∈ ℕ0s → ( -us ‘ 𝐴 ) ∈ Ons )
15		elons	⊢ ( ( -us ‘ 𝐴 ) ∈ Ons ↔ ( ( -us ‘ 𝐴 ) ∈ No ∧ ( R ‘ ( -us ‘ 𝐴 ) ) = ∅ ) )
16	15	simprbi	⊢ ( ( -us ‘ 𝐴 ) ∈ Ons → ( R ‘ ( -us ‘ 𝐴 ) ) = ∅ )
17	14 16	syl	⊢ ( ( -us ‘ 𝐴 ) ∈ ℕ0s → ( R ‘ ( -us ‘ 𝐴 ) ) = ∅ )
18	17	adantl	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( R ‘ ( -us ‘ 𝐴 ) ) = ∅ )
19	18	imaeq2d	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( -us “ ( R ‘ ( -us ‘ 𝐴 ) ) ) = ( -us “ ∅ ) )
20		ima0	⊢ ( -us “ ∅ ) = ∅
21	19 20	eqtrdi	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( -us “ ( R ‘ ( -us ‘ 𝐴 ) ) ) = ∅ )
22	10 13 21	3eqtr3d	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( L ‘ 𝐴 ) = ∅ )
23	22	ex	⊢ ( 𝐴 ∈ No → ( ( -us ‘ 𝐴 ) ∈ ℕ0s → ( L ‘ 𝐴 ) = ∅ ) )
24	6 23	orim12d	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( ( R ‘ 𝐴 ) = ∅ ∨ ( L ‘ 𝐴 ) = ∅ ) ) )
25	24	imp	⊢ ( ( 𝐴 ∈ No ∧ ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ) → ( ( R ‘ 𝐴 ) = ∅ ∨ ( L ‘ 𝐴 ) = ∅ ) )
26	25	orcomd	⊢ ( ( 𝐴 ∈ No ∧ ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ) → ( ( L ‘ 𝐴 ) = ∅ ∨ ( R ‘ 𝐴 ) = ∅ ) )
27	1 26	sylbi	⊢ ( 𝐴 ∈ ℤs → ( ( L ‘ 𝐴 ) = ∅ ∨ ( R ‘ 𝐴 ) = ∅ ) )