Metamath Proof Explorer

Theorem n0sfincut

Description: The simplest number greater than a finite set of non-negative surreal integers is a non-negative surreal integer. (Contributed by Scott Fenton, 5-Nov-2025)

Ref Expression
Assertion n0sfincut 
|- ( ( A C_ NN0_s /\ A e. Fin ) -> ( A |s (/) ) e. NN0_s )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( A = (/) -> ( A |s (/) ) = ( (/) |s (/) ) )
2 df-0s 
 |-  0s = ( (/) |s (/) )
3 0n0s 
 |-  0s e. NN0_s
4 2 3 eqeltrri 
 |-  ( (/) |s (/) ) e. NN0_s
5 1 4 eqeltrdi 
 |-  ( A = (/) -> ( A |s (/) ) e. NN0_s )
6 5 a1d 
 |-  ( A = (/) -> ( ( A C_ NN0_s /\ A e. Fin ) -> ( A |s (/) ) e. NN0_s ) )
7 n0ssno 
 |-  NN0_s C_ No
8 sstr 
 |-  ( ( A C_ NN0_s /\ NN0_s C_ No ) -> A C_ No )
9 7 8 mpan2 
 |-  ( A C_ NN0_s -> A C_ No )
10 sltso 
 |-
11 soss 
 |-  ( A C_ No -> (
12 9 10 11 mpisyl 
 |-  ( A C_ NN0_s ->
13 12 ad2antrl 
 |-  ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) ->
14 simprr 
 |-  ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) -> A e. Fin )
15 simpl 
 |-  ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) -> A =/= (/) )
16 fimax2g 
 |-  ( (  E. x e. A A. y e. A -. x
17 13 14 15 16 syl3anc 
 |-  ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) -> E. x e. A A. y e. A -. x
18 9 ad2antrl 
 |-  ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) -> A C_ No )
19 18 adantr 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ x e. A ) -> A C_ No )
20 19 sselda 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ x e. A ) /\ y e. A ) -> y e. No )
21 18 sselda 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ x e. A ) -> x e. No )
22 21 adantr 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ x e. A ) /\ y e. A ) -> x e. No )
23 slenlt 
 |-  ( ( y e. No /\ x e. No ) -> ( y <_s x <-> -. x
24 20 22 23 syl2anc 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ x e. A ) /\ y e. A ) -> ( y <_s x <-> -. x
25 24 ralbidva 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ x e. A ) -> ( A. y e. A y <_s x <-> A. y e. A -. x
26 simpl 
 |-  ( ( x e. A /\ A. y e. A y <_s x ) -> x e. A )
27 ssel2 
 |-  ( ( A C_ No /\ x e. A ) -> x e. No )
28 18 26 27 syl2an 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> x e. No )
29 snelpwi 
 |-  ( x e. No -> { x } e. ~P No )
30 nulssgt 
 |-  ( { x } e. ~P No -> { x } <
31 28 29 30 3syl 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> { x } <
32 breq2 
 |-  ( w = x -> ( x <_s w <-> x <_s x ) )
33 simprl 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> x e. A )
34 slerflex 
 |-  ( x e. No -> x <_s x )
35 28 34 syl 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> x <_s x )
36 32 33 35 rspcedvdw 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> E. w e. A x <_s w )
37 vex 
 |-  x e. _V
38 breq1 
 |-  ( z = x -> ( z <_s w <-> x <_s w ) )
39 38 rexbidv 
 |-  ( z = x -> ( E. w e. A z <_s w <-> E. w e. A x <_s w ) )
40 37 39 ralsn 
 |-  ( A. z e. { x } E. w e. A z <_s w <-> E. w e. A x <_s w )
41 36 40 sylibr 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> A. z e. { x } E. w e. A z <_s w )
42 ral0 
 |-  A. z e. (/) E. w e. (/) w <_s z
43 42 a1i 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> A. z e. (/) E. w e. (/) w <_s z )
44 simplrr 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> A e. Fin )
45 snex 
 |-  { ( { x } |s (/) ) } e. _V
46 45 a1i 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> { ( { x } |s (/) ) } e. _V )
47 18 adantr 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> A C_ No )
48 31 scutcld 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( { x } |s (/) ) e. No )
49 48 snssd 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> { ( { x } |s (/) ) } C_ No )
50 47 sselda 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> z e. No )
51 28 adantr 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> x e. No )
52 48 adantr 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> ( { x } |s (/) ) e. No )
53 breq1 
 |-  ( y = z -> ( y <_s x <-> z <_s x ) )
54 simplrr 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> A. y e. A y <_s x )
55 simpr 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> z e. A )
56 53 54 55 rspcdva 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> z <_s x )
57 51 34 syl 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> x <_s x )
58 breq2 
 |-  ( z = x -> ( x <_s z <-> x <_s x ) )
59 37 58 rexsn 
 |-  ( E. z e. { x } x <_s z <-> x <_s x )
60 57 59 sylibr 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> E. z e. { x } x <_s z )
61 60 orcd 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> ( E. z e. { x } x <_s z \/ E. w e. ( _Right ` x ) w <_s ( { x } |s (/) ) ) )
62 lltropt 
 |-  ( _Left ` x ) <
63 62 a1i 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> ( _Left ` x ) <
64 31 adantr 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> { x } <
65 lrcut 
 |-  ( x e. No -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x )
66 51 65 syl 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x )
67 66 eqcomd 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> x = ( ( _Left ` x ) |s ( _Right ` x ) ) )
68 eqidd 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> ( { x } |s (/) ) = ( { x } |s (/) ) )
69 sltrec 
 |-  ( ( ( ( _Left ` x ) < ( x  ( E. z e. { x } x <_s z \/ E. w e. ( _Right ` x ) w <_s ( { x } |s (/) ) ) ) )
70 63 64 67 68 69 syl22anc 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> ( x  ( E. z e. { x } x <_s z \/ E. w e. ( _Right ` x ) w <_s ( { x } |s (/) ) ) ) )
71 61 70 mpbird 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> x
72 50 51 52 56 71 slelttrd 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> z
73 velsn 
 |-  ( w e. { ( { x } |s (/) ) } <-> w = ( { x } |s (/) ) )
74 breq2 
 |-  ( w = ( { x } |s (/) ) -> ( z  z
75 73 74 sylbi 
 |-  ( w e. { ( { x } |s (/) ) } -> ( z  z
76 72 75 syl5ibrcom 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> ( w e. { ( { x } |s (/) ) } -> z
77 76 3impia 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A /\ w e. { ( { x } |s (/) ) } ) -> z
78 44 46 47 49 77 ssltd 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> A <
79 snelpwi 
 |-  ( ( { x } |s (/) ) e. No -> { ( { x } |s (/) ) } e. ~P No )
80 nulssgt 
 |-  ( { ( { x } |s (/) ) } e. ~P No -> { ( { x } |s (/) ) } <
81 48 79 80 3syl 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> { ( { x } |s (/) ) } <
82 31 41 43 78 81 cofcut1d 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( { x } |s (/) ) = ( A |s (/) ) )
83 82 eqcomd 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( A |s (/) ) = ( { x } |s (/) ) )
84 simplrl 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> A C_ NN0_s )
85 84 33 sseldd 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> x e. NN0_s )
86 peano2n0s 
 |-  ( x e. NN0_s -> ( x +s 1s ) e. NN0_s )
87 85 86 syl 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( x +s 1s ) e. NN0_s )
88 n0scut 
 |-  ( ( x +s 1s ) e. NN0_s -> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) )
89 87 88 syl 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) )
90 1sno 
 |-  1s e. No
91 pncans 
 |-  ( ( x e. No /\ 1s e. No ) -> ( ( x +s 1s ) -s 1s ) = x )
92 28 90 91 sylancl 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( ( x +s 1s ) -s 1s ) = x )
93 92 sneqd 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> { ( ( x +s 1s ) -s 1s ) } = { x } )
94 93 oveq1d 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) = ( { x } |s (/) ) )
95 89 94 eqtr2d 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( { x } |s (/) ) = ( x +s 1s ) )
96 95 87 eqeltrd 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( { x } |s (/) ) e. NN0_s )
97 83 96 eqeltrd 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( A |s (/) ) e. NN0_s )
98 97 expr 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ x e. A ) -> ( A. y e. A y <_s x -> ( A |s (/) ) e. NN0_s ) )
99 25 98 sylbird 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ x e. A ) -> ( A. y e. A -. x  ( A |s (/) ) e. NN0_s ) )
100 99 rexlimdva 
 |-  ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) -> ( E. x e. A A. y e. A -. x  ( A |s (/) ) e. NN0_s ) )
101 17 100 mpd 
 |-  ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) -> ( A |s (/) ) e. NN0_s )
102 101 ex 
 |-  ( A =/= (/) -> ( ( A C_ NN0_s /\ A e. Fin ) -> ( A |s (/) ) e. NN0_s ) )
103 6 102 pm2.61ine 
 |-  ( ( A C_ NN0_s /\ A e. Fin ) -> ( A |s (/) ) e. NN0_s )