Skip to content

Commit

Permalink
Replace "rn" by "cdm" (3c)
Browse files Browse the repository at this point in the history
See issue metamath#4470:

Label changes:
* ~smorndom  -> ~smocdmdom (used 2 times)
  • Loading branch information
avekens committed Jan 4, 2025
1 parent 922eb60 commit 02a2fb8
Show file tree
Hide file tree
Showing 2 changed files with 69 additions and 68 deletions.
1 change: 1 addition & 0 deletions changes-set.txt
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,7 @@ make a github issue.)

DONE:
Date Old New Notes
4-Jan-25 smorndom smocdmdom
2-Jan-25 frnnn0fsuppg fcdmnn0fsuppg
2-Jan-25 frnnn0suppg fcdmnn0suppg
2-Jan-25 frnnn0fsupp fcdmnn0fsupp
Expand Down
136 changes: 68 additions & 68 deletions set.mm
Original file line number Diff line number Diff line change
Expand Up @@ -82738,7 +82738,7 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $=
$d A x $. $d B x $. $d F x $.
$( The codomain of a strictly monotone ordinal function dominates the
domain. (Contributed by Mario Carneiro, 13-Mar-2013.) $)
smorndom $p |- ( ( F : A --> B /\ Smo F /\ Ord B ) -> A C_ B ) $=
smocdmdom $p |- ( ( F : A --> B /\ Smo F /\ Ord B ) -> A C_ B ) $=
( vx wf wsmo word w3a cv wcel wa cfv wss wfn simpl1 simpl2 smodm2 syl2anc
ffnd ordelord sylancom simpl3 simpr syl3anc ffvelcdm 3ad2antl1 ordtr2 imp
smogt syl22anc ex ssrdv ) ABCEZCFZBGZHZDABUPDIZAJZUQBJZUPURKZUQGZUOUQUQCL
Expand Down Expand Up @@ -109394,63 +109394,63 @@ _Cardinal Arithmetic_ (1994), p. xxx (Roman numeral 30). The cofinality
( con0 wcel wa cfv wss vt vs word wrex wral wsmo w3a wex csuc cdm wfo cep
cv wf wiso wf1o cvv wwe ssrab3 ssexg mpan onss sstrid epweon mpisyl oiiso
wess syl2anc ad2antlr isof1o f1ofo 3syl fof fss sylancl oion simplr eloni
syl smoiso2 syl2an biimpar simprd syl21anc smorndom syl3anc onsssuc mpbid
wb adantrr ccom vex oiexg coexg sylancr fcod simpr ordsson ad2antrr simpl
simprl ffvelcdm wfn ffn smoel2 sylan wi wceq fveq2 eleq2d raleqbi1dv crab
jca weq eleq1d cbvralvw bitrid cbvrabv eqtri elrab2 simprbi rspccv ordtr1
sylc ancomsd imp fvco3 syl2an2r 3eltr4d ralrimivva issmo2 syl13anc sseq2d
c0 cint ex wn ffvelcdmd mpd ralbidv rabn0 ssrab2 inteqi eqeltrid sylan2br
wne onint elrab sylib adantl simpr2 simp3 eleq2i simp21 simp1l fssd ontr1
simp22 simp1r 3impib ontri1 simp23 simpl1 sstr anim12i sylibr onnmin expr
rabid syl31anc sylbird con4d syl5bi 3expia ralrimiv sylanbrc expcom com13
3expib syld com23 imp31 foelrn biimpcd ad5ant24 sylancom sylibrd reximdva
eleq1 syl6 ralimdv impr 3jca feq1 smoeq fveq1 3anbi123d spcedv feq2 rexeq
rexbidv 3anbi13d exbidv rspcev exlimdv ) FUCZGPQZRZGFIUMZUNZCUMZDUMZUXISZ
TZDGUDZCFUEZRZAUMZFJUMZUNZUXSUFZUXKEUMZUXSSZTZEUXRUDZCFUEZUGZJUHZAGUIZUDZ
IUXHUXQUYJUXHUXQRZLUJZUYIQZUYLFUXSUNZUYAUYDEUYLUDZCFUEZUGZJUHZUYJUXHUXJUY
MUXPUXHUXJRZUYLGTZUYMUYSUYLGLUNZLUFZGUCZUYTUYSUYLHLUKZVUAUYSUYLHULULLUOZU
YLHLUPVUDUXGVUEUXFUXJUXGHUQQZHULURZVUEHGTZUXGVUFUXMBUMZUXISZQZDVUIUEZBGHM
USZHGPUTVAZUXGHPTZPULURVUGUXGHGPVUMGVBZVCZVDHPULVGVEHULLUQOVFVHVIZUYLHULU
LLVJUYLHLVKVLZVUDUYLHLUNZVUHVUAUYLHLVMZVUMUYLHGLVNVOVSZUYSUYLPQZUXGVUEVUB
UXGVVCUXFUXJUXGVUFVVCVUNHULLUQOVPVSVIZUXFUXGUXJVQZVURVVCUXGRZVUERVUDVUBVV
FVUDVUBRZVUEVVCUYLUCZVUOVVGVUEWIUXGUYLVRZVUQUYLHLVTWAWBWCWDZUXGVUCUXFUXJG
VRVIUYLGLWEWFUYSVVCUXGUYTUYMWIVVDVVEUYLGWGVHWHWJUYKUYQUYLFUXILWKZUNZVVKUF
ZUXKUYBVVKSZTZEUYLUDZCFUEZUGJUQVVKUYKUXIUQQLUQQZVVKUQQIWLUXGVVRUXFUXQUXGV
UFVVRVUNHULLUQOWMVSVIUXILUQUQWNWOUYKVVLVVMVVQUYKUYLGFUXILUXHUXJUXPXAUXHUX
JVUAUXPVVBWJWPUXHUXJVVMUXPUYSVVLFPTZVVHUAUMZVVKSZUBUMZVVKSZQZUAVWBUEUBUYL
UEZVVMUYSUYLGFUXILUXHUXJWQVVBWPUXFVVSUXGUXJFWRZWSUYSVVCVVHVVDVVIVSUYSVWDU
BUAUYLVWBUYSVWBUYLQZVVTVWBQZRZRZVVTLSZUXISZVWBLSZUXISZVWAVWCVWJVWMHQZVWKV
WMQZVWLVWNQZUYSVUTVWGVWOVWIUYSVUDVUTVUSVVAVSVWGVWHWTUYLHVWBLXBWAUYSLUYLXC
ZVUBRVWIVWPUYSVWRVUBUYSVUDVUTVWRVUSVVAUYLHLXDVLVVJXMUYLVWBVVTLXEXFVWOUXRU
XISZVWNQZAVWMUEZVWPVWQXGVWOVWMGQVXAVWSUXKUXISZQZAUXKUEZVXACVWMGHVXCVWTAUX
KVWMUXKVWMXHVXBVWNVWSUXKVWMUXIXIXJXKHVULBGXLVXDCGXLMVULVXDBCGVULVWSVUJQZA
VUIUEBCXNZVXDVUKVXEDAVUIDAXNZUXMVWSVUJUXLUXRUXIXIZXOXPVXEVXCAVUIUXKVXFVUJ
VXBVWSVUIUXKUXIXIXJXKXQXRXSXTYAVWTVWQAVWKVWMUXRVWKXHVWSVWLVWNUXRVWKUXIXIX
OYBVSYDUYSVUAVWIVVTUYLQZVWAVWLXHVVBUYSVWIVXIUYSVVCVVHVWIVXIXGVVDVVIVVHVWH
VWGVXIVVTVWBUYLYCYEVLYFUYLGVVTUXILYGYHUYSVUAVWIVWGVWCVWNXHVVBUYSVWGVWHXAU
YLGVWBUXILYGYHYIYJVVLVVSVVHVWEUGVVMUBUAUYLFVVKYKYFYLWJUXHUXJUXPVVQUYSUXOV
VPCFUYSUXOVVPUYSUXORZKUYBLSZXHZEUYLUDZVVPUYSVUDUXOKHQZVXMVUSUXHUXJUXOVXNU
XHUXOUXJVXNUXHUXOKGQZUXKKUXISZTZRZUXJVXNXGUXGUXOVXRXGUXFUXGUXOVXRUXGUXORZ
KUXNDGXLZQZVXRUXOUXGVXTYNUUFZVYAUXNDGUUAUXGVXTPTZVYBVYAUXGVXTGPUXNDGUUBVU
PVCZVYCVYBRKVXTYOZVXTKUXKVWSTZAGXLZYOVYENVYGVXTVYFUXNADGADXNVWSUXMUXKUXRU
XLUXIXIYMXRUUCXSZVXTUUGUUDXFUUEZUXNVXQDKGUXLKXHUXMVXPUXKUXLKUXIXIYMUUHUUI
YPUUJUXJVXRUXHVXNUXJVXOVXQUXHVXNXGUXHUXJVXOVXQUGZVXNUXHVYJRZVXOUXMVXPQZDK
UEZVXNUXHUXJVXOVXQUUKVYKVYLDKUXHVYJUXLKQZVYLUXHVYJVYNUGZVYNVYLUXHVYJVYNUU
LZVYNUXLVYEQZVYOVYLKVYEUXLVYHUUMVYOVYLVYQVYOVYLYQZVXPUXMTZVYQYQZVYOVXPPQU
XMPQVYSVYRWIVYOGPKUXIVYOGFPUXIUXHUXJVXOVXQVYNUUNVYOUXFVVSUXFUXGVYJVYNUUOV
WFVSUUPZUXHUXJVXOVXQVYNUURZYRVYOGPUXLUXIWUAVYOUXGVYNVXOUXLGQZUXFUXGVYJVYN
UUSZVYPWUBUXGVYNVXOWUCUXLKGUUQUUTZWFYRVXPUXMUVAVHVYOUXGVYNVXOVXQVYSVYTXGW
UDVYPWUBUXHUXJVXOVXQVYNUVBUXGVYNVXOUGZVXQVYSVYTWUFVXQVYSRZRZVYCUXLVXTQZVY
TWUHUXGVYCUXGVYNVXOWUGUVCVYDVSWUHWUCUXNRWUIWUFWUCWUGUXNWUEUXKVXPUXMUVDUVE
UXNDGUVIUVFVXTUXLUVGVHUVHUVJUVKUVLUVMYSUVNUVOVULVYMBKGHVUKVYLDVUIKVUIKXHV
UJVXPUXMVUIKUXIXIXJXKMXTUVPUVQUVSUVRUVTUWAUWBEUYLHKLUWCYHVXJVXLVVOEUYLVXJ
UYBUYLQZRZVXLUXKVXKUXISZTZVVOUXGUXOVXLWUMXGZUXFUXJWUJVXSVYAWUNVYIVYAVXLVX
KVXTQZWUMVXLVYAWUOKVXKVXTUWIUWDWUOVXKGQWUMVYFWUMAVXKGVXTUXRVXKXHVWSWULUXK
UXRVXKUXIXIYMUXNVYFDAGVXGUXMVWSUXKVXHYMXRXTYAUWJVSUWEWUKVVNWULUXKVXJWUJVU
AVVNWULXHUYSVUAUXOWUJVVBWSUYLGUYBUXILYGUWFYMUWGUWHYSYPUWKUWLUWMUXSVVKXHZU
YNVVLUYAVVMUYPVVQUYLFUXSVVKUWNUXSVVKUWOWUPUYOVVPCFWUPUYDVVOEUYLWUPUYCVVNU
XKUYBUXSVVKUWPYMUXAYTUWQUWRUYHUYRAUYLUYIUXRUYLXHZUYGUYQJWUQUXTUYNUYFUYPUY
AUXRUYLFUXSUWSWUQUYEUYOCFUYDEUXRUYLUWTYTUXBUXCUXDVHYPUXE $.
wb smoiso2 syl2an biimpar simprd syl21anc smocdmdom syl3anc onsssuc mpbid
syl adantrr ccom vex oiexg coexg sylancr simprl fcod simpr ad2antrr simpl
ordsson ffvelcdm wfn ffn jca smoel2 sylan wi wceq fveq2 eleq2d raleqbi1dv
crab weq eleq1d cbvralvw bitrid cbvrabv elrab2 simprbi rspccv sylc ordtr1
eqtri ancomsd fvco3 syl2an2r 3eltr4d ralrimivva issmo2 syl13anc c0 sseq2d
imp cint ex wn ffvelcdmd mpd ralbidv rabn0 ssrab2 onint eqeltrid sylan2br
inteqi elrab sylib adantl simpr2 simp3 eleq2i simp21 simp1l simp22 simp1r
wne fssd ontr1 3impib ontri1 simp23 simpl1 sstr anim12i rabid sylibr expr
onnmin syl31anc con4d syl5bi 3expia ralrimiv sylanbrc expcom 3expib com13
sylbird syld com23 imp31 eleq1 biimpcd ad5ant24 sylancom sylibrd reximdva
foelrn syl6 ralimdv impr 3jca feq1 smoeq fveq1 rexbidv 3anbi123d 3anbi13d
spcedv feq2 rexeq exbidv rspcev exlimdv ) FUCZGPQZRZGFIUMZUNZCUMZDUMZUXIS
ZTZDGUDZCFUEZRZAUMZFJUMZUNZUXSUFZUXKEUMZUXSSZTZEUXRUDZCFUEZUGZJUHZAGUIZUD
ZIUXHUXQUYJUXHUXQRZLUJZUYIQZUYLFUXSUNZUYAUYDEUYLUDZCFUEZUGZJUHZUYJUXHUXJU
YMUXPUXHUXJRZUYLGTZUYMUYSUYLGLUNZLUFZGUCZUYTUYSUYLHLUKZVUAUYSUYLHULULLUOZ
UYLHLUPVUDUXGVUEUXFUXJUXGHUQQZHULURZVUEHGTZUXGVUFUXMBUMZUXISZQZDVUIUEZBGH
MUSZHGPUTVAZUXGHPTZPULURVUGUXGHGPVUMGVBZVCZVDHPULVGVEHULLUQOVFVHVIZUYLHUL
ULLVJUYLHLVKVLZVUDUYLHLUNZVUHVUAUYLHLVMZVUMUYLHGLVNVOWIZUYSUYLPQZUXGVUEVU
BUXGVVCUXFUXJUXGVUFVVCVUNHULLUQOVPWIVIZUXFUXGUXJVQZVURVVCUXGRZVUERVUDVUBV
VFVUDVUBRZVUEVVCUYLUCZVUOVVGVUEVSUXGUYLVRZVUQUYLHLVTWAWBWCWDZUXGVUCUXFUXJ
GVRVIUYLGLWEWFUYSVVCUXGUYTUYMVSVVDVVEUYLGWGVHWHWJUYKUYQUYLFUXILWKZUNZVVKU
FZUXKUYBVVKSZTZEUYLUDZCFUEZUGJUQVVKUYKUXIUQQLUQQZVVKUQQIWLUXGVVRUXFUXQUXG
VUFVVRVUNHULLUQOWMWIVIUXILUQUQWNWOUYKVVLVVMVVQUYKUYLGFUXILUXHUXJUXPWPUXHU
XJVUAUXPVVBWJWQUXHUXJVVMUXPUYSVVLFPTZVVHUAUMZVVKSZUBUMZVVKSZQZUAVWBUEUBUY
LUEZVVMUYSUYLGFUXILUXHUXJWRVVBWQUXFVVSUXGUXJFXAZWSUYSVVCVVHVVDVVIWIUYSVWD
UBUAUYLVWBUYSVWBUYLQZVVTVWBQZRZRZVVTLSZUXISZVWBLSZUXISZVWAVWCVWJVWMHQZVWK
VWMQZVWLVWNQZUYSVUTVWGVWOVWIUYSVUDVUTVUSVVAWIVWGVWHWTUYLHVWBLXBWAUYSLUYLX
CZVUBRVWIVWPUYSVWRVUBUYSVUDVUTVWRVUSVVAUYLHLXDVLVVJXEUYLVWBVVTLXFXGVWOUXR
UXISZVWNQZAVWMUEZVWPVWQXHVWOVWMGQVXAVWSUXKUXISZQZAUXKUEZVXACVWMGHVXCVWTAU
XKVWMUXKVWMXIVXBVWNVWSUXKVWMUXIXJXKXLHVULBGXMVXDCGXMMVULVXDBCGVULVWSVUJQZ
AVUIUEBCXNZVXDVUKVXEDAVUIDAXNZUXMVWSVUJUXLUXRUXIXJZXOXPVXEVXCAVUIUXKVXFVU
JVXBVWSVUIUXKUXIXJXKXLXQXRYDXSXTVWTVWQAVWKVWMUXRVWKXIVWSVWLVWNUXRVWKUXIXJ
XOYAWIYBUYSVUAVWIVVTUYLQZVWAVWLXIVVBUYSVWIVXIUYSVVCVVHVWIVXIXHVVDVVIVVHVW
HVWGVXIVVTVWBUYLYCYEVLYNUYLGVVTUXILYFYGUYSVUAVWIVWGVWCVWNXIVVBUYSVWGVWHWP
UYLGVWBUXILYFYGYHYIVVLVVSVVHVWEUGVVMUBUAUYLFVVKYJYNYKWJUXHUXJUXPVVQUYSUXO
VVPCFUYSUXOVVPUYSUXORZKUYBLSZXIZEUYLUDZVVPUYSVUDUXOKHQZVXMVUSUXHUXJUXOVXN
UXHUXOUXJVXNUXHUXOKGQZUXKKUXISZTZRZUXJVXNXHUXGUXOVXRXHUXFUXGUXOVXRUXGUXOR
ZKUXNDGXMZQZVXRUXOUXGVXTYLUUQZVYAUXNDGUUAUXGVXTPTZVYBVYAUXGVXTGPUXNDGUUBV
UPVCZVYCVYBRKVXTYOZVXTKUXKVWSTZAGXMZYOVYENVYGVXTVYFUXNADGADXNVWSUXMUXKUXR
UXLUXIXJYMXRUUFYDZVXTUUCUUDXGUUEZUXNVXQDKGUXLKXIUXMVXPUXKUXLKUXIXJYMUUGUU
HYPUUIUXJVXRUXHVXNUXJVXOVXQUXHVXNXHUXHUXJVXOVXQUGZVXNUXHVYJRZVXOUXMVXPQZD
KUEZVXNUXHUXJVXOVXQUUJVYKVYLDKUXHVYJUXLKQZVYLUXHVYJVYNUGZVYNVYLUXHVYJVYNU
UKZVYNUXLVYEQZVYOVYLKVYEUXLVYHUULVYOVYLVYQVYOVYLYQZVXPUXMTZVYQYQZVYOVXPPQ
UXMPQVYSVYRVSVYOGPKUXIVYOGFPUXIUXHUXJVXOVXQVYNUUMVYOUXFVVSUXFUXGVYJVYNUUN
VWFWIUURZUXHUXJVXOVXQVYNUUOZYRVYOGPUXLUXIWUAVYOUXGVYNVXOUXLGQZUXFUXGVYJVY
NUUPZVYPWUBUXGVYNVXOWUCUXLKGUUSUUTZWFYRVXPUXMUVAVHVYOUXGVYNVXOVXQVYSVYTXH
WUDVYPWUBUXHUXJVXOVXQVYNUVBUXGVYNVXOUGZVXQVYSVYTWUFVXQVYSRZRZVYCUXLVXTQZV
YTWUHUXGVYCUXGVYNVXOWUGUVCVYDWIWUHWUCUXNRWUIWUFWUCWUGUXNWUEUXKVXPUXMUVDUV
EUXNDGUVFUVGVXTUXLUVIVHUVHUVJUVSUVKUVLYSUVMUVNVULVYMBKGHVUKVYLDVUIKVUIKXI
VUJVXPUXMVUIKUXIXJXKXLMXSUVOUVPUVQUVRUVTUWAUWBEUYLHKLUWIYGVXJVXLVVOEUYLVX
JUYBUYLQZRZVXLUXKVXKUXISZTZVVOUXGUXOVXLWUMXHZUXFUXJWUJVXSVYAWUNVYIVYAVXLV
XKVXTQZWUMVXLVYAWUOKVXKVXTUWCUWDWUOVXKGQWUMVYFWUMAVXKGVXTUXRVXKXIVWSWULUX
KUXRVXKUXIXJYMUXNVYFDAGVXGUXMVWSUXKVXHYMXRXSXTUWJWIUWEWUKVVNWULUXKVXJWUJV
UAVVNWULXIUYSVUAUXOWUJVVBWSUYLGUYBUXILYFUWFYMUWGUWHYSYPUWKUWLUWMUXSVVKXIZ
UYNVVLUYAVVMUYPVVQUYLFUXSVVKUWNUXSVVKUWOWUPUYOVVPCFWUPUYDVVOEUYLWUPUYCVVN
UXKUYBUXSVVKUWPYMUWQYTUWRUWTUYHUYRAUYLUYIUXRUYLXIZUYGUYQJWUQUXTUYNUYFUYPU
YAUXRUYLFUXSUXAWUQUYEUYOCFUYDEUXRUYLUXBYTUWSUXCUXDVHYPUXE $.
$}

${
Expand Down Expand Up @@ -111880,17 +111880,17 @@ version of the pigeonhole principle (for aleph-null pigeons and 2 holes)
( con0 wss cwdom wbr wa wcel cpw cdom word cep cvv 3syl wf adantr syl3anc
syl cdm char cfv oicl wb cuni csuc relwdom brrelex1i adantl uniexg sucexg
wsmo oif onsucuni fss sylancr crn wceq oismo simpld ssorduni ordsuc sylib
smorndom ssexd elong mpbiri csdm canth2g sdomdom cen wf1o wiso wwe epweon
simpl wess mpisyl epse oiiso2 sylancl isof1o simprd f1oeq3d mpbid f1oen2g
smocdmdom ssexd elong mpbiri csdm canth2g sdomdom cen wf1o wiso wwe simpl
wse epweon wess mpisyl oiiso2 sylancl isof1o simprd f1oeq3d mpbid f1oen2g
endom domwdom wdomtr sylancom wdompwdom domtr syl2anc elharval sylanbrc
wse ) AEFZABGHZIZCUAZEJZXABKZLHZXAXCUBUCJWTXBXAMZANCDUDWTXAOJZXBXEUEWTXAA
UFZUGZOWTAOJZXGOJXHOJWSXIWRABGUHUIUJZAOUKXGOULPWTXAXHCQZCUMZXHMZXAXHFWTXA
ACQAXHFZXKANCDUNWRXNWSAUORXAAXHCUPUQWTXLCURZAUSZWRXLXPIWSACDUTRZVAWTXGMZX
MWRXRWSAVBRXGVCVDXAXHCVESVFZXAOVGTVHZWTXAXAKZLHZYAXCLHZXDWTXFXAYAVIHYBXSX
AOVJXAYAVKPWTXABGHZYCWRWSXAAGHZYDWTXAAVLHZXAALHYEWTXBXIXAACVMZYFXTXJWTXAX
OCVMZYGWTXAXONNCVNZYHWTANVOZANWQYIWTWRENVOYJWRWSVQVPAENVRVSAVTANCDWAWBXAX
ONNCWCTWTXOAXACWTXLXPXQWDWEWFXAACEOWGSXAAWHXAAWIPXAABWJWKXABWLTXAYAXCWMWN
XCXAWOWP $.
epse ) AEFZABGHZIZCUAZEJZXABKZLHZXAXCUBUCJWTXBXAMZANCDUDWTXAOJZXBXEUEWTXA
AUFZUGZOWTAOJZXGOJXHOJWSXIWRABGUHUIUJZAOUKXGOULPWTXAXHCQZCUMZXHMZXAXHFWTX
AACQAXHFZXKANCDUNWRXNWSAUORXAAXHCUPUQWTXLCURZAUSZWRXLXPIWSACDUTRZVAWTXGMZ
XMWRXRWSAVBRXGVCVDXAXHCVESVFZXAOVGTVHZWTXAXAKZLHZYAXCLHZXDWTXFXAYAVIHYBXS
XAOVJXAYAVKPWTXABGHZYCWRWSXAAGHZYDWTXAAVLHZXAALHYEWTXBXIXAACVMZYFXTXJWTXA
XOCVMZYGWTXAXONNCVNZYHWTANVOZANVQYIWTWRENVOYJWRWSVPVRAENVSVTAWQANCDWAWBXA
XONNCWCTWTXOAXACWTXLXPXQWDWEWFXAACEOWGSXAAWHXAAWIPXAABWJWKXABWLTXAYAXCWMW
NXCXAWOWP $.
$}

${
Expand Down

0 comments on commit 02a2fb8

Please sign in to comment.