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 63 64 67 68 sltrecd 
 |-  ( ( ( ( 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 (/) ) ) ) )
70 61 69 mpbird 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> x
71 50 51 52 56 70 slelttrd 
 |-  ( ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) /\ z e. A ) -> z
72 velsn 
 |-  ( w e. { ( { x } |s (/) ) } <-> w = ( { x } |s (/) ) )
73 breq2 
 |-  ( w = ( { x } |s (/) ) -> ( z  z
74 72 73 sylbi 
 |-  ( w e. { ( { x } |s (/) ) } -> ( z  z
75 71 74 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
76 75 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
77 44 46 47 49 76 ssltd 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> A <
78 snelpwi 
 |-  ( ( { x } |s (/) ) e. No -> { ( { x } |s (/) ) } e. ~P No )
79 nulssgt 
 |-  ( { ( { x } |s (/) ) } e. ~P No -> { ( { x } |s (/) ) } <
80 48 78 79 3syl 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> { ( { x } |s (/) ) } <
81 31 41 43 77 80 cofcut1d 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( { x } |s (/) ) = ( A |s (/) ) )
82 81 eqcomd 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( A |s (/) ) = ( { x } |s (/) ) )
83 simplrl 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> A C_ NN0_s )
84 83 33 sseldd 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> x e. NN0_s )
85 peano2n0s 
 |-  ( x e. NN0_s -> ( x +s 1s ) e. NN0_s )
86 84 85 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 )
87 n0scut 
 |-  ( ( x +s 1s ) e. NN0_s -> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) )
88 86 87 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 (/) ) )
89 1sno 
 |-  1s e. No
90 pncans 
 |-  ( ( x e. No /\ 1s e. No ) -> ( ( x +s 1s ) -s 1s ) = x )
91 28 89 90 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 )
92 91 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 } )
93 92 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 (/) ) )
94 88 93 eqtr2d 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( { x } |s (/) ) = ( x +s 1s ) )
95 94 86 eqeltrd 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( { x } |s (/) ) e. NN0_s )
96 82 95 eqeltrd 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ ( x e. A /\ A. y e. A y <_s x ) ) -> ( A |s (/) ) e. NN0_s )
97 96 expr 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ x e. A ) -> ( A. y e. A y <_s x -> ( A |s (/) ) e. NN0_s ) )
98 25 97 sylbird 
 |-  ( ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) /\ x e. A ) -> ( A. y e. A -. x  ( A |s (/) ) e. NN0_s ) )
99 98 rexlimdva 
 |-  ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) -> ( E. x e. A A. y e. A -. x  ( A |s (/) ) e. NN0_s ) )
100 17 99 mpd 
 |-  ( ( A =/= (/) /\ ( A C_ NN0_s /\ A e. Fin ) ) -> ( A |s (/) ) e. NN0_s )
101 100 ex 
 |-  ( A =/= (/) -> ( ( A C_ NN0_s /\ A e. Fin ) -> ( A |s (/) ) e. NN0_s ) )
102 6 101 pm2.61ine 
 |-  ( ( A C_ NN0_s /\ A e. Fin ) -> ( A |s (/) ) e. NN0_s )