Metamath Proof Explorer

Theorem zscut0

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

Ref Expression
Assertion zscut0 
|- ( A e. ZZ_s -> ( ( _Left ` A ) = (/) \/ ( _Right ` A ) = (/) ) )

Proof

Step Hyp Ref Expression
1 elzn0s 
 |-  ( A e. ZZ_s <-> ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) )
2 n0ons 
 |-  ( A e. NN0_s -> A e. On_s )
3 elons 
 |-  ( A e. On_s <-> ( A e. No /\ ( _Right ` A ) = (/) ) )
4 3 simprbi 
 |-  ( A e. On_s -> ( _Right ` A ) = (/) )
5 2 4 syl 
 |-  ( A e. NN0_s -> ( _Right ` A ) = (/) )
6 5 a1i 
 |-  ( A e. No -> ( A e. NN0_s -> ( _Right ` A ) = (/) ) )
7 simpl 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> A e. No )
8 7 negscld 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us ` A ) e. No )
9 negsleft 
 |-  ( ( -us ` A ) e. No -> ( _Left ` ( -us ` ( -us ` A ) ) ) = ( -us " ( _Right ` ( -us ` A ) ) ) )
10 8 9 syl 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( _Left ` ( -us ` ( -us ` A ) ) ) = ( -us " ( _Right ` ( -us ` A ) ) ) )
11 negnegs 
 |-  ( A e. No -> ( -us ` ( -us ` A ) ) = A )
12 11 fveq2d 
 |-  ( A e. No -> ( _Left ` ( -us ` ( -us ` A ) ) ) = ( _Left ` A ) )
13 12 adantr 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( _Left ` ( -us ` ( -us ` A ) ) ) = ( _Left ` A ) )
14 n0ons 
 |-  ( ( -us ` A ) e. NN0_s -> ( -us ` A ) e. On_s )
15 elons 
 |-  ( ( -us ` A ) e. On_s <-> ( ( -us ` A ) e. No /\ ( _Right ` ( -us ` A ) ) = (/) ) )
16 15 simprbi 
 |-  ( ( -us ` A ) e. On_s -> ( _Right ` ( -us ` A ) ) = (/) )
17 14 16 syl 
 |-  ( ( -us ` A ) e. NN0_s -> ( _Right ` ( -us ` A ) ) = (/) )
18 17 adantl 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( _Right ` ( -us ` A ) ) = (/) )
19 18 imaeq2d 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us " ( _Right ` ( -us ` A ) ) ) = ( -us " (/) ) )
20 ima0 
 |-  ( -us " (/) ) = (/)
21 19 20 eqtrdi 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us " ( _Right ` ( -us ` A ) ) ) = (/) )
22 10 13 21 3eqtr3d 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( _Left ` A ) = (/) )
23 22 ex 
 |-  ( A e. No -> ( ( -us ` A ) e. NN0_s -> ( _Left ` A ) = (/) ) )
24 6 23 orim12d 
 |-  ( A e. No -> ( ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) -> ( ( _Right ` A ) = (/) \/ ( _Left ` A ) = (/) ) ) )
25 24 imp 
 |-  ( ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) -> ( ( _Right ` A ) = (/) \/ ( _Left ` A ) = (/) ) )
26 25 orcomd 
 |-  ( ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) -> ( ( _Left ` A ) = (/) \/ ( _Right ` A ) = (/) ) )
27 1 26 sylbi 
 |-  ( A e. ZZ_s -> ( ( _Left ` A ) = (/) \/ ( _Right ` A ) = (/) ) )