diff --git a/changes-set.txt b/changes-set.txt
index 9b7e6c1d8..e96b8fd3a 100644
--- a/changes-set.txt
+++ b/changes-set.txt
@@ -98,6 +98,9 @@ make a github issue.)
 DONE:
 Date      Old       New         Notes
 30-Sep-24 syl5req   eqtr2id     compare to eqtr2i or eqtr2d
+27-Sep-24 syldbl2   [same]      moved from SP's mathbox to main set.mm
+27-Sep-24 fiminre2  [same]      moved from GS's mathbox to main set.mm
+27-Sep-24 infrefilb [same]      moved from GS's mathbox to main set.mm
 22-Sep-24 grpcld    [same]      moved from SN's mathbox to main set.mm
 21-Sep-24 sb56      sbalex      substitution expressed with 'al' or with 'ex'
 21-Sep-24 nanimn    dfnan2      mark as an alternative definition
diff --git a/discouraged b/discouraged
index 2d36eb77e..f89cb7a32 100644
--- a/discouraged
+++ b/discouraged
@@ -465,17 +465,6 @@
 "5oalem5" is used by "5oalem6".
 "5oalem6" is used by "5oalem7".
 "5oalem7" is used by "5oai".
-"abeq2" is used by "abeq1".
-"abeq2" is used by "bj-ru1".
-"abeq2" is used by "clabel".
-"abeq2" is used by "dfss2OLD".
-"abeq2" is used by "dmopab3".
-"abeq2" is used by "fineqvrep".
-"abeq2" is used by "funimaexg".
-"abeq2" is used by "rabid2".
-"abeq2" is used by "ru".
-"abeq2" is used by "sbcabel".
-"abeq2" is used by "zfrep4".
 "ablo32" is used by "ablo4".
 "ablo32" is used by "ip0i".
 "ablo32" is used by "nvadd32".
@@ -13940,7 +13929,6 @@ New usage of "ab0ALT" is discouraged (0 uses).
 New usage of "ab0OLD" is discouraged (0 uses).
 New usage of "ab0orvALT" is discouraged (0 uses).
 New usage of "abbiOLD" is discouraged (0 uses).
-New usage of "abeq2" is discouraged (11 uses).
 New usage of "abfOLD" is discouraged (0 uses).
 New usage of "ablo32" is discouraged (4 uses).
 New usage of "ablo4" is discouraged (3 uses).
diff --git a/set.mm b/set.mm
index 4b3dbc694..d150e6846 100644
--- a/set.mm
+++ b/set.mm
@@ -7199,6 +7199,14 @@ _praeclarum theorema_ (splendid theorem).  (Contributed by NM,
       ( wa jca syl21anc ) ABCLDEFABCGHMIJKN $.
   $}
 
+  ${
+    syldbl2.1 $e |- ( ( ph /\ ps ) -> ( ps -> th ) ) $.
+    $( Stacked hypotheseis implies goal.  (Contributed by Stanislas Polu,
+       9-Mar-2020.) $)
+    syldbl2 $p |- ( ( ph /\ ps ) -> th ) $=
+      ( wa com12 anabsi7 ) ABCABEBCDFG $.
+  $}
+
   ${
     mpsyl4anc.1 $e |- ph $.
     mpsyl4anc.2 $e |- ps $.
@@ -26527,7 +26535,7 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
        equivalent formulation ~ cplem2 .  For more information on class
        variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13.
        Usage of ~ abeq2w is preferred since it requires fewer axioms.
-       (Contributed by NM, 26-May-1993.)  (New usage is discouraged.) $)
+       (Contributed by NM, 26-May-1993.) $)
     abeq2 $p |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) ) $=
       ( vy cab wceq cv wcel wb wal ax-5 hbab1 cleqh abid bibi2i albii bitri ) C
       ABEZFBGZCHZSRHZIZBJTAIZBJBDCRDGCHBKABDLMUBUCBUAATABNOPQ $.
@@ -127129,6 +127137,20 @@ Ordering on reals (cont.)
       PCDVDRUJVAVPVEDGVNCDVERUKULVTVSSVQVRVFUOTVTVGSVQVFVDVEUMTUNUPUQURUSUT $.
   $}
 
+  ${
+    $d A x y $.
+    $( A nonempty finite set of real numbers is bounded below.  (Contributed by
+       Glauco Siliprandi, 8-Apr-2021.) $)
+    fiminre2 $p |- ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A x <_ y )
+               $=
+      ( cr wss cfn wcel wa c0 wceq cle wbr wral wrex cc0 0red rzal breq1 adantl
+      cv ralbidv rspcev syl2anc wn wne neqne simpll simplr simpr fiminre ssrexv
+      syl3anc sylc syldan pm2.61dan ) CDEZCFGZHZCIJZATZBTZKLZBCMZADNZUSVDURUSOD
+      GOVAKLZBCMZVDUSPVEBCQVCVFAODUTOJVBVEBCUTOVAKRUAUBUCSURUSUDZCIUEZVDVGVHURC
+      IUFSURVHHZUPVCACNZVDUPUQVHUGZVIUPUQVHVJVKUPUQVHUHURVHUIABCUJULVCACDUKUMUN
+      UO $.
+  $}
+
   ${
     $d A a n x $.
     $( The negation of a finite set of real numbers is finite.  (Contributed by
@@ -127762,6 +127784,17 @@ Dedekind cut construction of the reals (see ~ df-mp ).  (Contributed by
       $.
   $}
 
+  ${
+    $d B x y $.
+    $( The infimum of a finite set of reals is less than or equal to any of its
+       elements.  (Contributed by Glauco Siliprandi, 8-Apr-2021.) $)
+    infrefilb $p |- ( ( B C_ RR /\ B e. Fin /\ A e. B ) -> inf ( B , RR , < )
+       <_ A ) $=
+      ( vx vy cr wss cfn wcel w3a cle wbr wral wrex cinf simp1 fiminre2 3adant3
+      cv clt simp3 infrelb syl3anc ) BEFZBGHZABHZIUCCRDRJKDBLCEMZUEBESNAJKUCUDU
+      EOUCUDUFUECDBPQUCUDUETCDABUAUB $.
+  $}
+
   ${
     supfirege.1 $e |- ( ph -> B C_ RR ) $.
     supfirege.2 $e |- ( ph -> B e. Fin ) $.
@@ -645010,6 +645043,383 @@ fixed reference functional determined by this vector (corresponding to
       UWHUUDRYTUWHUUTEUYLUYKYTUXOUUEYSYKYOYRTUJYDEVHSAUUFRCDUUG $.
   $}
 
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Sticks and stones
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+  ${
+    $d A f $.  $d I j x y $.  $d I j z $.  $d K f x y $.  $d K j x y $.
+    $d K j z $.  $d N a $.  $d N f $.  $d X f x y $.  $d X j x y $.
+    $d X j z $.  $d Y f x y $.  $d Y j x y $.  $d Y j z $.  $d a ph $.
+    $d f ph $.  $d j ph $.
+    sticksstones1.1 $e |- ( ph -> N e. NN0 ) $.
+    sticksstones1.2 $e |- ( ph -> K e. NN0 ) $.
+    sticksstones1.3 $e |- A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x
+    e. ( 1 ... K ) A. y e. ( 1 ... K )
+    ( x < y -> ( f ` x ) < ( f ` y ) ) ) } $.
+    sticksstones1.4 $e |- ( ph -> X e. A ) $.
+    sticksstones1.5 $e |- ( ph -> Y e. A ) $.
+    sticksstones1.6 $e |- ( ph -> X =/= Y ) $.
+    sticksstones1.7 $e |- I = inf ( { z e. ( 1 ... K ) |
+     ( X ` z ) =/= ( Y ` z ) } , RR , < ) $.
+    $( Different strictly monotone functions have different ranges.
+       (Contributed by metakunt, 27-Sep-2024.) $)
+    sticksstones1 $p  |- ( ph -> ran X =/= ran Y ) $=
+      ( clt wcel va vj cfv wbr wo crn wne cv c1 cfz co crab cr cinf wceq a1i c0
+      cfn wss w3a syl2anc wral wn nne bitri wa wfn wb wf wi feq1 breq12d imbi2d
+      fveq1 2ralbidv anbi12d adantl ralrimiva rspcdva simpld ffnd mpdan syldbl2
+      adantr ex imp cn fz1ssnn sstrd sseldd mpbird fveq2 neeq12d syl mpbid nfcv
+      nfv elfznn nnre ffvelrnd wnel wfun cdm ffund fdmd eleqtrrd 3ad2ant3 nnred
+      fvelrn lttri4d simp3 sseli simprd simpl3 breq1 breq1d breq2 breq2d rspc2v
+      3ad2ant1 imbi12d mpd cle sylib 3expa 3adantl2 ltned necomd neeq1d 3jaodan
+      simpl2 lttrd neneqd wrex ralnex nnel fvelrnb bitrd con1bid elnelne1 fzfid
+      wor ltso ssrab2 ssfi rabeq0 ralbii cab wal abeq2 spi biimpi eqfnfv bicomd
+      mpbi biimpd sylan2b necon3d nnssre 3jca fiinfcl eleq1d elrab3 ssrd lttri2
+      w3o simp2 3ad2ant2 ltnled infrefilb 3expia con3d elrabf notbii ianor imor
+      eqeltrd sylibr eqcomd jaodan ) AGJUCZGKUCZSUDZUWBUWASUDZUEZJUFZKUFZUGZAUW
+      AUWBUGZUWEAGDUHZJUCZUWJKUCZUGZDUIHUJUKZULZTZUWIAGUWOUMSUNZUWOGUWQUOZARUPZ
+      AUMSUUBZUWOURTZUWOUQUGZUWOUMUSZUTUWQUWOTUWTAUUCUPAUXAUXBUXCAUWNURTUWOUWNU
+      SZUXAAUIHUUAUXDAUWMDUWNUUDUPZUWNUWOUUEVAZAJKUGZUXBQAUXGUXBAUWOUQJKAUWOUQU
+      OZJKUOZUXHAUWKUWLUOZDUWNVBZUXIUXHUWMVCZDUWNVBUXKUWMDUWNUUFUXLUXJDUWNUWKUW
+      LVDUUGVEAUXKUXIAUXKVFZUXKUXIUXMUXIUXKUXMJUWNVGZKUWNVGZUXIUXKVHAUXNUXKAUWN
+      UIIUJUKZJAUWNUXPJVIZBUHZCUHZSUDZUXRJUCZUXSJUCZSUDZVJZCUWNVBBUWNVBZAUWNUXP
+      FUHZVIZUXTUXRUYFUCZUXSUYFUCZSUDZVJZCUWNVBBUWNVBZVFZUXQUYEVFFEJUYFJUOZUYGU
+      XQUYLUYEUWNUXPUYFJVKUYNUYKUYDBCUWNUWNUYNUYJUYCUXTUYNUYHUYAUYIUYBSUXRUYFJV
+      NUXSUYFJVNVLVMVOVPAUYMFEUYFETZUYMAUYOUYMUYOUYMVHZFEUYMFUUHUOUYPFUUINUYMFE
+      UUJUUOUUKUULVQVRZOVSZVTZWAZWDAUXOUXKAUWNUXPKAUWNUXPKVIZUXTUXRKUCZUXSKUCZS
+      UDZVJZCUWNVBBUWNVBZAKETZVUAVUFVFZPAVUHVUGAUYMVUHFEKUYFKUOZUYGVUAUYLVUFUWN
+      UXPUYFKVKVUIUYKVUEBCUWNUWNVUIUYJVUDUXTVUIUYHVUBUYIVUCSUXRUYFKVNUXSUYFKVNV
+      LVMVOVPUYQPVSZWDWBVTZWAZWDDUWNJKUUMVAUUNUUPWCUUQWEUURWFWBAUWOUWNUMUXEAUWN
+      WGUMUWNWGUSAHWHUPWGUMUSAUUSUPWIZWIZUUTUMUWOSUVAVAZUVQAGUWNTZUWPUWIVHAVUPU
+      WQUWNTAUWOUWNUWQUXEVUOWJAGUWQUWNUWSUVBWKZUWMUWIDGUWNUWJGUOUWKUWAUWLUWBUWJ
+      GJWLUWJGKWLWMUVCWNWOZAUWAUMTZUWBUMTZUWIUWEVHAUXPUMUWAAUAUXPUMAUAWQUAUXPWP
+      UAUMWPAUAUHZUXPTZVVAUMTZAVVBVFVVAWGTZVVCVVBVVDAVVAIWRVQVVAWSWNWEUVDZAUWNU
+      XPGJUYSVUQWTWJZAUXPUMUWBVVEAUWNUXPGKVUKVUQWTWJZUWAUWBUVEVAWOAUWCUWHUWDAUW
+      CVFZUWAUWFTZUWAUWGXAZUWHVVHJXBZGJXCZTZVVIAVVKUWCAUWNUXPJUYSXDWDAVVMUWCAGU
+      WNVVLVUQAUWNUXPJUYSXEXFWDGJXIVAVVHUBUHZKUCZUWAUOZVCZUBUWNVBZVVJVVHVVQUBUW
+      NVVHVVNUWNTZVFVVOUWAAUWCVVSVVOUWAUGZAUWCVVSUTZVVNGSUDZVVNGUOZGVVNSUDZUVFZ
+      VVTVWAVVNGVWAVVNVVSAVVNWGTZUWCVVNHWRZXGXHAUWCGUMTZVVSAUWNUMGVUMVUQWJZXTXJ
+      VWAVWBVVTVWCVWDVWAVWBVFZVVOUWAVWAVVOUMTZVWBVWAVVOUXPTZVWKVWAUWNUXPVVNKAUW
+      CVUAVVSVUKXTAUWCVVSXKZWTVWLVVOWGTVWKUXPWGVVOIWHZXLVVOWSWNWNZWDVWJVVOUWASU
+      DVVNJUCZUWASUDZVWAVWBVWQVWJUYEVWBVWQVJZVWAUYEVWBAUWCUYEVVSAUXQUYEUYRXMZXT
+      WDVWJVVSVUPUYEVWRVJAUWCVVSVWBXNVWAVUPVWBAUWCVUPVVSVUQXTZWDUYDVWRVVNUXSSUD
+      ZVWPUYBSUDZVJBCVVNGUWNUWNUXRVVNUOZUXTVXAUYCVXBUXRVVNUXSSXOZVXCUYAVWPUYBSU
+      XRVVNJWLXPYAUXSGUOZVXAVWBVXBVWQUXSGVVNSXQZVXEUYBUWAVWPSUXSGJWLXRYAXSVAYBW
+      CVWJVVOVWPUWASVWJVWPVVOAVVSVWBVWPVVOUOZUWCAVVSVWBVXGAVVSVWBUTZVVSVXGAVVSV
+      WBUVGVXHVVSVFVWPVVOUGZVCZVXGVXHVVSVXJVXHVVSVCVXJUEZVVSVXJVJVXHVVNUWOTZVCZ
+      VXKVXHGVVNYCUDZVCZVXMVXHVWBVXOAVVSVWBXKVXHVVNGVXHVVNVVSAVWFVWBVWGUVHXHAVV
+      SVWHVWBVWIXTUVIWOVXHVXLVXNVXHVXLVXNVXHVXLVFZVXNUWQVVNYCUDZVXHVXLVXQVXHUXC
+      UXAVXLVXQVJAVVSUXCVWBVUNXTAVVSUXAVWBUXFXTUXCUXAVXLVXQVVNUWOUVJUVKVAWFVXPG
+      UWQVVNYCUWRVXPRUPXPWKWEUVLYBVXMVVSVXIVFZVCVXKVXLVXRUWMVXIDVVNUWNDVVNWPDUW
+      NWPVXIDWQUWJVVNUOUWKVWPUWLVVOUWJVVNJWLUWJVVNKWLWMUVMUVNVVSVXIUVOVEYDVVSVX
+      JUVPUVRWFVWPVVOVDYDWBYEZYFUVSXPWKYGVWAVWCVFZVVTUWBUWAUGZVXTUWAUWBVWAUWIVW
+      CAUWCUWIVVSVURXTWDYHVWCVVTVYAVHVWAVWCVVOUWBUWAVVNGKWLYIVQWKVWAVWDVFZUWAVV
+      OVYBUWAVVOVWAVUSVWDAUWCVUSVVSVVFXTWDZVYBUWAUWBVVOVYCVWAVUTVWDAUWCVUTVVSVV
+      GXTWDVWAVWKVWDVWOWDAUWCVVSVWDYKVWAVWDUWBVVOSUDZVYBVUFVWDVYDVJZVWAVUFVWDAU
+      WCVUFVVSAVUAVUFVUJXMZXTWDVYBVUPVVSVUFVYEVJVWAVUPVWDVWTWDVWAVVSVWDVWMWDVUE
+      VYEGUXSSUDZUWBVUCSUDZVJBCGVVNUWNUWNUXRGUOZUXTVYGVUDVYHUXRGUXSSXOZVYIVUBUW
+      BVUCSUXRGKWLXPYAUXSVVNUOZVYGVWDVYHVYDUXSVVNGSXQZVYKVUCVVOUWBSUXSVVNKWLXRY
+      AXSVAYBWCYLYGYHYJWBYEYMVRAVVRVVJVHUWCAVVRVVPUBUWNYNZVCZVVJVVRVYNVHAVVPUBU
+      WNYOUPAVVJVYMAVVJVCZUWAUWGTZVYMVYOVYPVHAUWAUWGYPUPAUXOVYPVYMVHVULUBUWNUWA
+      KYQWNYRYSYRWDWOUWAUWFUWGYTVAAUWDVFZUWBUWGTZUWBUWFXAZUWHVYQKXBZGKXCZTZVYRA
+      VYTUWDAUWNUXPKVUKXDWDAWUBUWDAGUWNWUAVUQAUWNUXPKVUKXEXFWDGKXIVAVYQVWPUWBUO
+      ZVCZUBUWNVBZVYSVYQWUDUBUWNVYQVVSVFVWPUWBAUWDVVSVWPUWBUGZAUWDVVSUTZVWEWUFW
+      UGVVNGWUGVVNVVSAVWFUWDVWGXGXHAUWDVWHVVSVWIXTXJWUGVWBWUFVWCVWDWUGVWBVFZVWP
+      UWBWUGVWPUMTZVWBWUGVWPWUGVWPUXPTVWPWGTWUGUWNUXPVVNJAUWDUXQVVSUYSXTAUWDVVS
+      XKZWTUXPWGVWPVWNXLWNXHZWDWUHVWPUWBSUDVVOUWBSUDZWUGVWBWULWUHVUFVWBWULVJZWU
+      GVUFVWBAUWDVUFVVSVYFXTWDWUHVVSVUPVUFWUMVJAUWDVVSVWBXNWUGVUPVWBAUWDVUPVVSV
+      UQXTZWDVUEWUMVXAVVOVUCSUDZVJBCVVNGUWNUWNVXCUXTVXAVUDWUOVXDVXCVUBVVOVUCSUX
+      RVVNKWLXPYAVXEVXAVWBWUOWULVXFVXEVUCUWBVVOSUXSGKWLXRYAXSVAYBWCWUHVWPVVOUWB
+      SAVVSVWBVXGUWDVXSYFXPWKYGWUGVWCVFZWUFUWIWUPUWBUWAWUPUWBUWAWUGVUTVWCAUWDVU
+      TVVSVVGXTZWDAUWDVVSVWCYKYGYHVWCWUFUWIVHWUGVWCVWPUWAUWBVVNGJWLYIVQWKWUGVWD
+      VFZUWBVWPWURUWBVWPWUGVUTVWDWUQWDZWURUWBUWAVWPWUSWUGVUSVWDAUWDVUSVVSVVFXTW
+      DWUGWUIVWDWUKWDAUWDVVSVWDYKWUGVWDUWAVWPSUDZWURUYEVWDWUTVJZWUGUYEVWDAUWDUY
+      EVVSVWSXTWDWURVUPVVSUYEWVAVJWUGVUPVWDWUNWDWUGVVSVWDWUJWDUYDWVAVYGUWAUYBSU
+      DZVJBCGVVNUWNUWNVYIUXTVYGUYCWVBVYJVYIUYAUWAUYBSUXRGJWLXPYAVYKVYGVWDWVBWUT
+      VYLVYKUYBVWPUWASUXSVVNJWLXRYAXSVAYBWCYLYGYHYJWBYEYMVRAWUEVYSVHUWDAWUEWUCU
+      BUWNYNZVCZVYSWUEWVDVHAWUCUBUWNYOUPAVYSWVCAVYSVCZUWBUWFTZWVCWVEWVFVHAUWBUW
+      FYPUPAUXNWVFWVCVHUYTUBUWNUWBJYQWNYRYSYRWDWOVYRVYSVFUWGUWFUWBUWGUWFYTYHVAU
+      VTWB $.
+  $}
+
+  ${
+    $d A a b z $.  $d A f i j z $.  $d B z $.  $d F i j $.  $d K a b x y $.
+    $d K f x y $.  $d K r s $.  $d N a $.  $d N f $.  $d a b ph z $.
+    $d f i j ph z $.  $d i j r s $.  $d i j r x y $.  $d x y z $.
+    sticksstones2.1 $e |- ( ph -> N e. NN0 ) $.
+    sticksstones2.2 $e |- ( ph -> K e. NN0 ) $.
+    sticksstones2.3 $e |- B = { a e. ~P ( 1 ... N ) | ( # ` a ) = K } $.
+    sticksstones2.4 $e |- A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x
+    e. ( 1 ... K ) A. y e. ( 1 ... K )
+    ( x < y -> ( f ` x ) < ( f ` y ) ) ) } $.
+    sticksstones2.5 $e |- F = ( z e. A |-> ran z ) $.
+    $( The range function on strictly monotone functions with finite domain and
+       codomain is an injective mapping onto ` K ` -elemental sets.
+       (Contributed by metakunt, 27-Sep-2024.) $)
+    sticksstones2 $p  |- ( ph -> F : A -1-1-> B ) $=
+      ( cfv wceq wcel clt vi vj vb vs vr wf cv wi wral wa wf1 crn chash cfz cpw
+      c1 co crab fveqeq2 cfn fzfid wbr eleq1w feq1 fveq1 breq12d imbi2d ralbidv
+      wb anbi12d bibi12d cab wal abeq2 spi chvarvv biimpi adantl simpld sselpwd
+      mpbi frnd wfn hashfn syl cn0 adantr hashfz1 eqtrd eqcomd w3a wne wo cr cn
+      ffnd elfznn 3ad2ant3 nnred lttri2 syl2anc 3adant3 simp3 simpr breq1 fveq2
+      ffvelrnd simprd breq1d imbi12d breq2 breq2d rspc2v ltned ffvelrnda necomd
+      mpd jaodan ex sylbid necon4d ralrimiva 3expa dff13 sylibr hashf1rn elrabd
+      imp eleq2i mpbird fmptd cinf 3ad2ant1 simpl2 simpl3 rneqd 2ralbidv fvmptd
+      jca a1i neeq12d cbvrabv infeq1i sticksstones1 cmpt 3adant2 3netr4d ) AEFH
+      UFZUAUGZHQZUBUGZHQZRUUIUUKRUHZUBEUIZUAEUIZUJEFHUKAUUHUUOADEDUGZULZFHAUUPE
+      SZUJZUUQFSZUUQKUGZUMQIRZKUPJUNUQZUOZURZSZUUSUVBUUQUMQZIRKUUQUVDUVAUUQIUMU
+      SUUSUUQUVCUTUUSUPJVAUUSUPIUNUQZUVCUUPUUSUVHUVCUUPUFZBUGZCUGZTVBZUVJUUPQZU
+      VKUUPQZTVBZUHZCUVHUIZBUVHUIZUURUVIUVRUJZAUURUVSGUGZESZUVHUVCUVTUFZUVLUVJU
+      VTQZUVKUVTQZTVBZUHZCUVHUIZBUVHUIZUJZVIZUURUVSVIGDUVTUUPRZUWAUURUWIUVSGDEV
+      CUWKUWBUVIUWHUVRUVHUVCUVTUUPVDUWKUWGUVQBUVHUWKUWFUVPCUVHUWKUWEUVOUVLUWKUW
+      CUVMUWDUVNTUVJUVTUUPVEUVKUVTUUPVEVFVGVHVHVJVKUWJGEUWIGVLRUWJGVMOUWIGEVNWA
+      VOZVPVQVRZVSZWBVTUUSIUVGUUSIUUPUMQZUVGUUSUWOIUUSUWOUVHUMQZIUUSUUPUVHWCUWO
+      UWPRUUSUVHUVCUUPUWNWPUVHUUPWDWEUUSIWFSZUWPIRAUWQUURMWGIWHWEWIWJUUSUVHUTSU
+      VHUVCUUPUKZUWOUVGRUUSUPIVAUUSUVIUVAUUPQZUCUGZUUPQZRUVAUWTRUHZUCUVHUIZKUVH
+      UIZUJUWRUUSUVIUXDUWNUUSUXCKUVHAUURUVAUVHSZUXCAUURUXEWKZUXBUCUVHUXFUWTUVHS
+      ZUJZUVAUWTUWSUXAUXHUVAUWTWLZUVAUWTTVBZUWTUVATVBZWMZUWSUXAWLZUXHUVAWNSZUWT
+      WNSZUXIUXLVIUXFUXNUXGUXFUVAUXEAUVAWOSUURUVAIWQWRWSWGUXGUXOUXFUXGUWTUWTIWQ
+      WSVRUVAUWTWTXAUXHUXLUXMUXHUXJUXMUXKUXHUXJUJZUWSUXAUXPUWSUXPUWSUVCSZUWSWOS
+      UXHUXQUXJUXFUXQUXGUXFUVHUVCUVAUUPAUURUVIUXEUWNXBZAUURUXEXCZXGWGWGUWSJWQWE
+      WSUXHUXJUWSUXATVBZUXHUVRUXJUXTUHZUXFUVRUXGAUURUVRUXEUUSUVIUVRUWMXHXBWGZUX
+      HUXEUXGUVRUYAUHUXFUXEUXGUXSWGZUXFUXGXDZUVPUYAUVAUVKTVBZUWSUVNTVBZUHBCUVAU
+      WTUVHUVHUVJUVARZUVLUYEUVOUYFUVJUVAUVKTXEUYGUVMUWSUVNTUVJUVAUUPXFXIXJUVKUW
+      TRZUYEUXJUYFUXTUVKUWTUVATXKUYHUVNUXAUWSTUVKUWTUUPXFXLXJXMXAXQYHXNUXHUXKUJ
+      ZUXAUWSUYIUXAUWSUXHUXAWNSUXKUXHUXAUXHUXAUVCSUXAWOSUXFUVHUVCUWTUUPUXRXOUXA
+      JWQWEWSWGUXHUXKUXAUWSTVBZUXHUVRUXKUYJUHZUYBUXHUXGUXEUVRUYKUHUYDUYCUVPUYKU
+      WTUVKTVBZUXAUVNTVBZUHBCUWTUVAUVHUVHUVJUWTRZUVLUYLUVOUYMUVJUWTUVKTXEUYNUVM
+      UXAUVNTUVJUWTUUPXFXIXJUVKUVARZUYLUXKUYMUYJUVKUVAUWTTXKUYOUVNUWSUXATUVKUVA
+      UUPXFXLXJXMXAXQYHXNXPXRXSXTYAYBYCYBYSKUCUVHUVCUUPYDYEUVHUVCUUPUTYFXAWIWJY
+      GUUTUVFVIUUSFUVEUUQNYIYTYJPYKAUUNUAEAUUIESZUJZUUMUBEAUYPUUKESZUUMAUYPUYRW
+      KZUUIUUKUUJUULUYSUUIUUKWLZUUJUULWLUYSUYTUJZUUIULZUUKULZUUJUULVUABCUDEGUEU
+      GZUUIQZVUDUUKQZWLZUEUVHURZWNTYLIJUUIUUKUYSJWFSZUYTAUYPVUIUYRLYMWGUYSUWQUY
+      TAUYPUWQUYRMYMWGOAUYPUYRUYTYNZAUYPUYRUYTYOZUYSUYTXDWNVUHUDUGZUUIQZVULUUKQ
+      ZWLZUDUVHURTVUGVUOUEUDUVHVUDVULRVUEVUMVUFVUNVUDVULUUIXFVUDVULUUKXFUUAUUBU
+      UCUUDVUADUUIUUQVUBEHUVDHDEUUQUUERVUAPYTZVUAUUPUUIRZUJUUPUUIVUAVUQXDYPVUJV
+      UAVUBUVCUTVUAUPJVAVUAUVHUVCUUIUYSUVHUVCUUIUFZUYTAUYPVURUYRUYQVURUVLUVJUUI
+      QZUVKUUIQZTVBZUHZCUVHUIBUVHUIZUYPVURVVCUJZAUYPVVDUWJUYPVVDVIGUAUVTUUIRZUW
+      AUYPUWIVVDGUAEVCVVEUWBVURUWHVVCUVHUVCUVTUUIVDVVEUWFVVBBCUVHUVHVVEUWEVVAUV
+      LVVEUWCVUSUWDVUTTUVJUVTUUIVEUVKUVTUUIVEVFVGYQVJVKUWLVPVQVRVSXBWGWBVTYRVUA
+      DUUKUUQVUCEHUVDVUPVUAUUPUUKRZUJUUPUUKVUAVVFXDYPVUKUYSVUCUVDSUYTUYSVUCUVCU
+      TAUYPUVCUTSUYRAUPJVAYMUYSUVHUVCUUKAUYRUVHUVCUUKUFZUYPAUYRUJVVGUVLUVJUUKQZ
+      UVKUUKQZTVBZUHZCUVHUIBUVHUIZUYRVVGVVLUJZAUYRVVMUWJUYRVVMVIGUBUVTUUKRZUWAU
+      YRUWIVVMGUBEVCVVNUWBVVGUWHVVLUVHUVCUVTUUKVDVVNUWFVVKBCUVHUVHVVNUWEVVJUVLV
+      VNUWCVVHUWDVVITUVJUVTUUKVEUVKUVTUUKVEVFVGYQVJVKUWLVPVQVRVSUUFWBVTWGYRUUGX
+      SYAYCYBYBYSUAUBEFHYDYE $.
+  $}
+
+  ${
+    $d A a w $.  $d A f v z $.  $d B c w $.  $d B v w x y $.  $d B v x y z $.
+    $d F v w $.  $d K a x y $.  $d K f x y $.  $d N a $.  $d N f $.
+    $d a ph w x y $.  $d a ph x y z $.  $d c ph w $.  $d f ph v x y z $.
+    sticksstones3.1 $e |- ( ph -> N e. NN0 ) $.
+    sticksstones3.2 $e |- ( ph -> K e. NN0 ) $.
+    sticksstones3.3 $e |- B = { a e. ~P ( 1 ... N ) | ( # ` a ) = K } $.
+    sticksstones3.4 $e |- A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x
+    e. ( 1 ... K ) A. y e. ( 1 ... K )
+    ( x < y -> ( f ` x ) < ( f ` y ) ) ) } $.
+    sticksstones3.5 $e |- F = ( z e. A |-> ran z ) $.
+    $( The range function on strictly monotone functions with finite domain and
+       codomain is an surjective mapping onto ` K ` -elemental sets.
+       (Contributed by metakunt, 28-Sep-2024.) $)
+    sticksstones3 $p  |- ( ph -> F : A -onto-> B ) $=
+      ( wral wa wcel clt vw vv vc wfo cfv wceq wrex wf1 sticksstones2 ccnv wfun
+      wf cv df-f1 biimpi simpld syl wex c1 chash cfz co wiso wor cfn cr wss w3a
+      cn crab eleq2i adantl fveqeq2 elrab sylib elpwid sseld 3impa elfznn nnred
+      cpw imp 3expa ex ssrdv ltso mpi fzfid ssfid fz1iso syl2anc wbr wi cab cvv
+      soss wf1o wb df-isom 3ad2ant3 simprd f1oeq2d biimpd 3adant3 mpd f1of ffnd
+      oveq2 ovexd fnexd fss biimp a1i ralimdva adantr oveq2d raleqdv raleqbidva
+      mpbid jca feq1 fveq1 breq12d imbi2d 2ralbidv anbi12d elabd crn cmpt simpr
+      sylibr rneqd rnexg fvmptd 3ad2ant1 wfn dff1o2 simp3d eqtrd eqcomd eximdv
+      df-rex ralrimiva dffo3 mpbird ) AEFHUDZEFHULZUAUMZUBUMZHUEZUFZUBEUGZUAFQZ
+      RZAUUGUUMAEFHUHZUUGABCDEFGHIJKLMNOPUIUUOUUGHUJUKZUUOUUGUUPREFHUNUOUPUQAUU
+      LUAFAUUHFSZRZUUIESZUUKRZUBURZUULUURUSUUHUTUEZVAVBZUUHTTUUIVCZUBURZUVAUURU
+      UHTVDZUUHVESUVEUURUUHVFVGZUVFUURUCUUHVFUURUCUMZUUHSZUVHVFSZAUUQUVIUVJAUUQ
+      UVIVHZUVHUVKUVHUSJVAVBZSZUVHVISAUUQUVIUVMUURUVIUVMUURUUHUVLUVHUURUUHUVLUU
+      RUUHUVLWAZSZUVBIUFZUURUUHKUMZUTUEIUFZKUVNVJZSZUVOUVPRUUQUVTAUUQUVTFUVSUUH
+      NVKUOVLUVRUVPKUUHUVNUVQUUHIUTVMVNVOZUPVPZVQWBVRUVHJVSUQVTWCWDWEUVGVFTVDUV
+      FWFUUHVFTWPWGUQUURUVLUUHUURUSJWHUWBWIUUHTUBWJWKUURUVDUUTUBUURUVDUUTAUUQUV
+      DUUTAUUQUVDVHZUUSUUKUWCUUIUSIVAVBZUVLGUMZULZBUMZCUMZTWLZUWGUWEUEZUWHUWEUE
+      ZTWLZWMZCUWDQBUWDQZRZGWNZSUUSUWCUWOUWDUVLUUIULZUWIUWGUUIUEZUWHUUIUEZTWLZW
+      MZCUWDQZBUWDQZRGUUIWOUWCUWDUUIWOUWCUWDUUHUUIUWCUWDUUHUUIWQZUWDUUHUUIULZUW
+      CUVCUUHUUIWQZUXDUWCUXFUWIUWTWRZCUVCQZBUVCQZUVDAUXFUXIRZUUQUVDUXJBCUVCUUHT
+      TUUIWSUOWTZUPAUUQUXFUXDWMUVDUURUXFUXDUURUVPUXFUXDWRUURUVOUVPUWAXAZUVPUVCU
+      WDUUHUUIUVBIUSVAXHXBUQXCXDXEZUWDUUHUUIXFUQZXGUWCUSIVAXIXJUWCUWQUXCUWCUXEU
+      UHUVLVGZUWQUXNAUUQUXOUVDUWBXDUWDUUHUVLUUIXKWKUWCUXACUVCQZBUVCQZUXCUWCUXIU
+      XQUWCUXFUXIUXKXAUWCUXHUXPBUVCUWCUWGUVCSZRZUXGUXACUVCUXGUXAWMUXSUWHUVCSRUW
+      IUWTXLXMXNXNXEUWCUXPUXBBUVCUWDUWCUVBIUSVAAUUQUVDUVPUURUVPUVDUXLXOVRXPZUWC
+      UXPUXBWRUXRUWCUXACUVCUWDUXTXQXOXRXSXTUWEUUIUFZUWFUWQUWNUXCUWDUVLUWEUUIYAU
+      YAUWMUXABCUWDUWDUYAUWLUWTUWIUYAUWJUWRUWKUWSTUWGUWEUUIYBUWHUWEUUIYBYCYDYEY
+      FYGEUWPUUIOVKYKZUWCUUJUUHUWCUUJUUIYHZUUHUWCUUSUUJUYCUFZUYBAUUQUUSUYDWMUVD
+      AUUSUYDAUUSRZDUUIDUMZYHZUYCEHWOHDEUYGYIUFUYEPXMUYEUYFUUIUFZRUYFUUIUYEUYHY
+      JYLAUUSYJZUYEUUSUYCWOSUYIUUIEYMUQYNWDYOXEUWCUXDUYCUUHUFZUXMUXDUUIUWDYPZUU
+      IUJUKZUYJUXDUYKUYLUYJVHUWDUUHUUIYQUOYRUQYSYTXTWCWDUUAXEUUKUBEUUBYKUUCXTUU
+      FUUNWRAUBUAEFHUUDXMUUE $.
+  $}
+
+  ${
+    $d A a p $.  $d A f p $.  $d A g p $.  $d B g p $.  $d B p x y $.
+    $d K a x y $.  $d K f x y $.  $d N a $.  $d N f $.  $d a p ph x y $.
+    $d f p ph x y $.  $d g p ph $.
+    sticksstones4.1 $e |- ( ph -> N e. NN0 ) $.
+    sticksstones4.2 $e |- ( ph -> K e. NN0 ) $.
+    sticksstones4.3 $e |- B = { a e. ~P ( 1 ... N ) | ( # ` a ) = K } $.
+    sticksstones4.4 $e |- A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x
+    e. ( 1 ... K ) A. y e. ( 1 ... K )
+    ( x < y -> ( f ` x ) < ( f ` y ) ) ) } $.
+    $( Equinumerosity lemma for sticks and stones.  (Contributed by metakunt,
+       28-Sep-2024.) $)
+    sticksstones4 $p  |- ( ph -> A ~~ B ) $=
+      ( vg vp cv cvv c1 wcel cfn wf1o wex cen wbr crn cmpt wf1 wa sticksstones2
+      wfo eqid sticksstones3 jca df-f1o sylibr cfz co wf clt cfv wral cab simpl
+      wi wss a1i ss2abdv fzfid mapex syl2anc ssexg eleq1i mptexd f1oeq1 biimprd
+      wceq adantl spcimedv mpd bren ) ADENPZUAZNUBZDEUCUDADEODOPUEZUFZUAZWCADEW
+      EUGZDEWEUJZUHWFAWGWHABCODEFWEGHIJKLMWEUKZUIABCODEFWEGHIJKLMWIULUMDEWEUNUO
+      AWBWFNWEQAODWDQARGUPUQZRHUPUQZFPZURZBPZCPZUSUDWNWLUTWOWLUTUSUDVDCWJVABWJV
+      AZUHZFVBZQSZDQSAWRWMFVBZVEWTQSZWSAWQWMFWQWMVDAWMWPVCVFVGAWJTSWKTSXAARGVHA
+      RHVHWJWKTTFVIVJWRWTQVKVJDWRQMVLUOVMWAWEVPZWFWBVDAXBWBWFDEWAWEVNVOVQVRVSDE
+      NVTUO $.
+  $}
+
+  ${
+    $d A f $.  $d A s $.  $d K f x y $.  $d K s x y $.  $d N f x y $.
+    $d N s x y $.  $d f ph x y $.  $d ph s x y $.
+    sticksstones5.1 $e |- ( ph -> N e. NN0 ) $.
+    sticksstones5.2 $e |- ( ph -> K e. NN0 ) $.
+    sticksstones5.3 $e |- A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x
+    e. ( 1 ... K ) A. y e. ( 1 ... K )
+    ( x < y -> ( f ` x ) < ( f ` y ) ) ) } $.
+    $( Count the number of strictly monotonely increasing functions on finite
+       domains and codomains.  (Contributed by metakunt, 28-Sep-2024.) $)
+    sticksstones5 $p  |- ( ph -> ( # ` A ) = ( N _C K ) ) $=
+      ( vs chash cfv wceq c1 co cbc syl wcel eqtrd cv cfz cpw crab cen wbr eqid
+      sticksstones4 hasheni cfn cz fzfid nn0zd hashbc syl2anc eqcomd cn0 oveq1d
+      hashfz1 ) ADLMZKUALMFNKOGUBPZUCUDZLMZGFQPZADVBUEUFUTVCNABCDVBEFGKHIVBUGJU
+      HDVBUIRAVCVALMZFQPZVDAVFVCAVAUJSFUKSVFVCNAOGULAFIUMKVAFUNUOUPAVEGFQAGUQSV
+      EGNHGUSRURTT $.
+  $}
+
+  ${
+    $d G x $.  $d K x $.  $d X i x $.  $d Y i x $.  $d i ph x $.
+    sticksstones6.1 $e |- ( ph -> N e. NN0 ) $.
+    sticksstones6.2 $e |- ( ph -> K e. NN0 ) $.
+    sticksstones6.3 $e |- ( ph -> G : ( 1 ... ( K + 1 ) ) --> NN0 ) $.
+    sticksstones6.4 $e |- ( ph -> X e. ( 1 ... K ) ) $.
+    sticksstones6.5 $e |- ( ph -> Y e. ( 1 ... K ) ) $.
+    sticksstones6.6 $e |- ( ph -> X < Y ) $.
+    sticksstones6.7 $e |- F = ( x e. ( 1 ... K ) |-> ( x + sum_ i e.
+    ( 1 ... x ) ( G ` i ) ) ) $.
+    $( Function induces an order isomorphism for sticks and stones theorem.
+       (Contributed by metakunt, 1-Oct-2024.) $)
+    sticksstones6 $p |- ( ph -> ( F ` X ) < ( F ` Y ) ) $=
+      ( c1 co wcel adantr cfz cv cfv csu caddc clt cn elfznn syl nnred fzfid wa
+      cn0 1zzd cz nn0zd peano2zd adantl nnzd nnge1d cle wbr elfzle2 letrd lep1d
+      zred elfzd simpr ffvelrnd adantlr mpdan fsumnn0cl nn0red elfzelz readdcld
+      wf 1red cr ltp1d ltled elfzle1 fsumrecl nn0ge0d fsumge0 addge01d ltleaddd
+      cc0 mpbid cmpt wceq oveq2d sumeq1d oveq12d nnnn0d nn0addcld fvmptd eqcomd
+      a1i cin c0 fzdisj cun fzsplit recnd fsumsplit eqtrd 3brtr3d ) AHQHUARZCUB
+      ZEUCZCUDZUERZIXKHQUERZIUARZXJCUDZUERZUERZHDUCZIDUCZUFAHXKIXPAHAHQFUARZSZH
+      UGSZMHFUHUIZUJZAXKAXHXJCAQHUKAXIXHSZULZXIQFQUERZUARZSZXJUMSZYFXIQYGYFUNYF
+      FAFUOSZYEAFKUPZTZUQZYFXIYEXIUGSAXIHUHURZUSYFXIYOUTYFXIFYGYFXIYOUJZYFFYMVF
+      ZYFYGYNVFYFXIHFYPYFHAYBYEYCTUJYQYEXIHVAVBAXIQHVCURAHFVAVBZYEAYAYRMHQFVCUI
+      TVDYFFYQVEVDVGAYIYJYEAYIULYHUMXIEAYHUMEVPYILTAYIVHVIZVJVKVLZVMZAIAIXTSZIU
+      GSNIFUHUIZUJZAXKXOUUAAXNXJCAXMIUKZAXIXNSZULZXJUUGYIYJUUGXIQYGUUGUNUUGFAYK
+      UUFYLTZUQZUUFXIUOSZAXIXMIVNURZUUGQXMXIUUGVQZUUGHQAHVRSUUFYDTUULVOUUGXIUUK
+      VFZAQXMVAVBUUFAQHXMAVQZYDAHQYDUUNVOZAHYCUTZAHXMYDUUOAHYDVSZVTVDTUUFXMXIVA
+      VBAXIXMIWAURVDUUGXIIYGUUMAIVRSZUUFUUDTZUUGYGUUIVFZUUFXIIVAVBZAXIXMIVCURUU
+      GIFYGUUSUUGFUUHVFZUUTAIFVAVBZUUFAUUBUVCNIQFVCUIZTUUGFUVBVEVDVDVGAYIYJUUFY
+      SVJVKZVMZWBZVOOAWGXOVAVBXKXPVAVBAXNXJCUUEUVFUUGXJUVEWCWDAXKXOUUAUVGWEWHWF
+      AXRXLABHBUBZQUVHUARZXJCUDZUERZXLXTDUMDBXTUVKWIWJAPWRZAUVHHWJZULZUVHHUVJXK
+      UEAUVMVHZUVNUVIXHXJCUVNUVHHQUAUVOWKWLWMMAHXKAHYCWNZYTWOWPWQAXSXQAXSIQIUAR
+      ZXJCUDZUERZXQABIUVKUVSXTDUMUVLAUVHIWJZULZUVHIUVJUVRUEAUVTVHZUWAUVIUVQXJCU
+      WAUVHIQUAUWBWKWLWMNAIUVRAIUUCWNZAUVQXJCAQIUKZAXIUVQSZULZYIYJUWFXIQYGUWFUN
+      UWFFAYKUWEYLTZUQZUWEUUJAXIQIVNURZUWEQXIVAVBAXIQIWAURUWFXIIYGUWFXIUWIVFAUU
+      RUWEUUDTZUWFYGUWHVFZUWEUVAAXIQIVCURUWFIFYGUWJUWFFUWGVFZUWKAUVCUWEUVDTUWFF
+      UWLVEVDVDVGAYIYJUWEYSVJVKZVLWOWPAUVRXPIUEAXHXNXJUVQCAHXMUFVBXHXNWSWTWJUUQ
+      QHXMIXAUIAHUVQSUVQXHXNXBWJAHQIAUNAIUWCUPAHUVPUPUUPAHIYDUUDOVTVGHQIXCUIUWD
+      UWFXJUWFXJUWMVMXDXEWKXFWQXG $.
+  $}
+
+  ${
+    $d G x $.  $d K i x $.  $d X i x $.  $d i ph x $.
+    sticksstones7.1 $e |- ( ph -> N e. NN0 ) $.
+    sticksstones7.2 $e |- ( ph -> K e. NN0 ) $.
+    sticksstones7.3 $e |- ( ph -> G : ( 1 ... ( K + 1 ) ) --> NN0 ) $.
+    sticksstones7.4 $e |- ( ph -> X e. ( 1 ... K ) ) $.
+    sticksstones7.5 $e |- F = ( x e. ( 1 ... K ) |-> ( x + sum_ i e.
+    ( 1 ... x ) ( G ` i ) ) ) $.
+    sticksstones7.6 $e |- ( ph -> sum_ i e. ( 1 ... ( K + 1 ) )
+    ( G ` i ) = N ) $.
+    $( Closure property of sticks and stones function.  (Contributed by
+       metakunt, 1-Oct-2024.) $)
+    sticksstones7 $p |- ( ph -> ( F ` X ) e. ( 1 ... ( N + K ) ) ) $=
+      ( c1 co caddc wcel cle wbr cfv cfz cv csu cn0 cmpt wceq a1i simpr sumeq1d
+      wa oveq2d oveq12d cn elfznn syl nnnn0d fzfid 1zzd cz nn0zd adantr elfzelz
+      peano2zd adantl elfzle1 zred cr nnred elfzle2 nn0red readdcld lep1d letrd
+      1red elfzd wf ffvelrnda mpdan fsumnn0cl nn0addcld fvmptd zaddcld cc0 eqid
+      1p0e1 eqtr4i 0red nnge1d nn0ge0d le2addd eqbrtrd adantlr addge01d clt cin
+      mpbid c0 ltp1d fzdisj cun fzsplit nn0cn fsumsplit breqtrrd eqcomd addcomd
+      cc nn0cnd breqtrd eqeltrd ) AHDUAHOHUBPZCUCZEUAZCUDZQPZOGFQPZUBPABHBUCZOX
+      RUBPZXNCUDZQPZXPOFUBPZDUEDBYBYAUFUGAMUHAXRHUGZUKZXRHXTXOQAYCUIZYDXSXLXNCY
+      DXRHOUBYEULUJUMLAHXOAHAHYBRZHUNRLHFUOUPZUQZAXLXNCAOHURAXMXLRZUKZXMOFOQPZU
+      BPZRZXNUERZYJXMOYKYJUSYJFAFUTRYIAFJVAZVBVDZYIXMUTRZAXMOHVCVEZYIOXMSTAXMOH
+      VFVEYJXMHYKYJXMYRVGAHVHRZYIAHYGVIZVBYJYKYPVGYIXMHSTAXMOHVJVEAHYKSTYIAHFYK
+      YTAFJVKZAFOUUAAVOZVLAYFHFSTLHOFVJUPZAFUUAVMVNZVBVNVPYJYLUEXMEAYLUEEVQYIKV
+      BVRVSVTZWAZWBAXPOXQAUSZAGFAGIVAYOWCAXPUUFVAAOOWDQPZXPSOUUHUGAOOUUHOWEWFWG
+      UHAOWDHXOUUBAWHYTAXOUUEVKZAHYGWIZAXOUUEWJWKWLAXPFGQPXQSAHXOFGYTUUIUUAAGIV
+      KUUCAXOYLXNCUDZGSAXOXOHOQPZYKUBPZXNCUDZQPZUUKSAWDUUNSTXOUUOSTAUUNAUUMXNCA
+      UULYKURAXMUUMRZUKZYMYNUUQXMOYKAOUTRUUPUUGVBAYKUTRUUPAFYOVDZVBUUPYQAXMUULY
+      KVCVEZUUQOUULXMAOVHRUUPUUBVBZUUQHOAYSUUPYTVBZUUTVLZUUQXMUUSVGUUQOHUULUUTU
+      VAUVBAOHSTUUPUUJVBUUQHUVAVMVNUUPUULXMSTAXMUULYKVFVEVNUUPXMYKSTAXMUULYKVJV
+      EVPAYMYNUUPAYLUEXMEKVRZWMVSVTZWJAXOUUNUUIAUUNUVDVKWNWQAXLUUMXNYLCAHUULWOT
+      XLUUMWPWRUGAHYTWSOHUULYKWTUPAHYLRYLXLUUMXAUGAHOYKUUGUURAHYHVAUUJUUDVPHOYK
+      XBUPAOYKURAYMUKYNXNXHRUVCXNXCUPXDXEAUUKGNXFXEWKAFGAFJXIAGIXIXGXJVPXK $.
+  $}
+
+
+  ${
+    $d A a e j l $.  $d A a j l x y $.  $d B a $.  $d K e j l $.
+    $d K f j l x y $.  $d K g i $.  $d N f j $.  $d N g $.  $d a f j l x y $.
+    $d a g i $.  $d a e j l ph $.  $d i l $.  $d ph x y $.
+    sticksstones8.1 $e |- ( ph -> N e. NN0 ) $.
+    sticksstones8.2 $e |- ( ph -> K e. NN0 ) $.
+    sticksstones8.3 $e |- F = ( a e. A |-> ( j e. ( 1 ... K ) |->
+    ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) ) $.
+    sticksstones8.4 $e |- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\
+     sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } $.
+    sticksstones8.5 $e |- B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) )
+    /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y ->
+    ( f ` x ) < ( f ` y ) ) ) } $.
+    $( Establish mapping between strictly monotone functions and functions that
+       sum to a fixed non-negative integer.  (Contributed by metakunt,
+       1-Oct-2024.) $)
+    sticksstones8 $p |- ( ph -> F : A --> B ) $=
+      ( wcel ve c1 cfz co cv cfv csu caddc cmpt wa wf clt wbr wi wral cab eqidd
+      w3a cvv wceq simpr oveq2d sumeq1d oveq12d simp3 ovexd fvmptd cn0 3ad2ant1
+      eqcomd eleqtrrd wb feq1 simpl fveq1d sumeq2dv eqeq1d anbi12d elabg biimpd
+      a1i syl mpd simpld 3adant3 eqid fveq2 cbvsum simprd eqtr3id sticksstones7
+      eqeltrrd 3expa fmptd ad3antrrr adantr adantl simpllr simplr sticksstones6
+      nfcv ex ralrimiva jca cfn fzfid fexd fveq1 breq12d imbi2d 2ralbidv mpbird
+      ) AMDIUBKUCUDZIUEZUBXNUCUDZNUEZMUEZUFZNUGZUHUDZUIZEJAXQDTZUJZYAXMUBLKUHUD
+      UCUDZFUEZUKZBUEZCUEZULUMZYGYEUFZYHYEUFZULUMZUNZCXMUOBXMUOZUJZFUPZEYCYAYPT
+      ZXMYDYAUKZYIYGYAUFZYHYAUFZULUMZUNZCXMUOZBXMUOZUJZYCYRUUDYCIXMXTYDYAAYBXNX
+      MTZXTYDTAYBUUFURZXNUAXMUAUEZUBUUHUCUDZXRNUGZUHUDZUIZUFXTYDUUGUAXNUUKXTXMU
+      ULUSUUGUULUQUUGUUHXNUTZUJZUUHXNUUJXSUHUUGUUMVAZUUNUUIXOXRNUUNUUHXNUBUCUUO
+      VBVCVDAYBUUFVEZUUGXNXSUHVFVGUUGUANUULXQKLXNAYBLVHTZUUFOVIAYBKVHTZUUFPVIAY
+      BUBKUBUHUDUCUDZVHXQUKZUUFYCUUTUUSHUEZXQUFZHUGZLUTZYCXQUUSVHGUEZUKZUUSUVAU
+      VEUFZHUGZLUTZUJZGUPZTZUUTUVDUJZYCXQDUVKAYBVAZYCDUVKDUVKUTYCRWAVJVKZYCUVLU
+      VMYCYBUVLUVMVLZUVNUVJUVMGXQDUVEXQUTZUVFUUTUVIUVDUUSVHUVEXQVMUVQUVHUVCLUVQ
+      UUSUVGUVBHUVQUVAUUSTZUJUVAUVEXQUVQUVRVNVOVPVQVRVSZWBVTWCZWDWEUUPUULWFAYBU
+      USXRNUGZLUTUUFYCUWAUVCLUUSUVBXRHNUVAXPXQWGNUUSXAHUUSXANUVBXAHXRXAWHYCUUTU
+      VDUVTWIWJWEWKWLWMYAWFZWNZYCUUCBXMYCYGXMTZUJZUUBCXMUWEYHXMTZUJZYIUUAUWGYIU
+      JINYAXQKLYGYHUWGUUQYIAUUQYBUWDUWFOWOWPUWGUURYIAUURYBUWDUWFPWOWPUWGUUTYIUW
+      EUUTUWFYCUUTUWDYCUUTUVDYCUVLUVMUVOYCUVLUVMYBUVPAUVSWQVTWCWDWPWPWPYCUWDUWF
+      YIWRUWEUWFYIWSUWGYIVAUWBWTXBXCXCXDYCYAUSTYQUUEVLYCXMYDXEYAUWCYCUBKXFXGYOU
+      UEFYAUSYEYAUTZYFYRYNUUDXMYDYEYAVMUWHYMUUBBCXMXMUWHYLUUAYIUWHYJYSYKYTULYGY
+      EYAXHYHYEYAXHXIXJXKVRVSWBXLEYPUTYCSWAVKQWN $.
+  $}
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -674885,14 +675295,6 @@ base set if and only if the neighborhoods (convergents) of every point
       QCVPTAVTVCVDVEAIBCDEGVFVGFAJBCDEGVFVI $.
   $}
 
-  ${
-    syldbl2.1 $e |- ( ( ph /\ ps ) -> ( ps -> th ) ) $.
-    $( Stacked hypotheseis implies goal.  (Contributed by Stanislas Polu,
-       9-Mar-2020.) $)
-    syldbl2 $p |- ( ( ph /\ ps ) -> th ) $=
-      ( wa com12 anabsi7 ) ABCABEBCDFG $.
-  $}
-
   ${
     $d A x y $.  $d A z $.  $d B z $.
     suprlubrd.1 $e |- ( ph -> A C_ RR ) $.
@@ -694216,20 +694618,6 @@ not even needed (it can be any class).  (Contributed by Glauco
       $.
   $}
 
-  ${
-    $d A x y $.
-    $( A nonempty finite set of real numbers is bounded below.  (Contributed by
-       Glauco Siliprandi, 8-Apr-2021.) $)
-    fiminre2 $p |- ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A x <_ y )
-               $=
-      ( cr wss cfn wcel wa c0 wceq cle wbr wral wrex cc0 0red rzal breq1 adantl
-      cv ralbidv rspcev syl2anc wn wne neqne simpll simplr simpr fiminre ssrexv
-      syl3anc sylc syldan pm2.61dan ) CDEZCFGZHZCIJZATZBTZKLZBCMZADNZUSVDURUSOD
-      GOVAKLZBCMZVDUSPVEBCQVCVFAODUTOJVBVEBCUTOVAKRUAUBUCSURUSUDZCIUEZVDVGVHURC
-      IUFSURVHHZUPVCACNZVDUPUQVHUGZVIUPUQVHVJVKUPUQVHUHURVHUIABCUJULVCACDUKUMUN
-      UO $.
-  $}
-
   $( The set of positive integers is nonempty.  (Contributed by Glauco
      Siliprandi, 8-Apr-2021.) $)
   nnn0 $p |- NN =/= (/) $=
@@ -694257,17 +694645,6 @@ not even needed (it can be any class).  (Contributed by Glauco
   fzossuz $p |- ( M ..^ N ) C_ ( ZZ>= ` M ) $=
     ( cfzo co cfz cuz cfv fzossfz fzssuz sstri ) ABCDABEDAFGABHABIJ $.
 
-  ${
-    $d B x y $.
-    $( The infimum of a finite set of reals is less than or equal to any of its
-       elements.  (Contributed by Glauco Siliprandi, 8-Apr-2021.) $)
-    infrefilb $p |- ( ( B C_ RR /\ B e. Fin /\ A e. B ) -> inf ( B , RR , < )
-       <_ A ) $=
-      ( vx vy cr wss cfn wcel w3a cle wbr wral wrex cinf simp1 fiminre2 3adant3
-      cv clt simp3 infrelb syl3anc ) BEFZBGHZABHZIUCCRDRJKDBLCEMZUEBESNAJKUCUDU
-      EOUCUDUFUECDBPQUCUDUETCDABUAUB $.
-  $}
-
   ${
     $d A x y $.
     $( The real and extended real infima match when the set is finite.