Skip to content

Commit

Permalink
Rename syl6sseqr to sseqtrrdi (#3789)
Browse files Browse the repository at this point in the history 
This is in set.mm and iset.mm

Co-authored-by: Wolf Lammen <[email protected]>
  • Loading branch information
@jkingdon @wlammen
jkingdon and wlammen authored Jan 25, 2024
1 parent 259bd9b commit 4d51170
Show file tree
Hide file tree
Showing 3 changed files with 235 additions and 235 deletions.
2 changes: 1 addition & 1 deletion changes-set.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,6 @@ proposed syl6eleq eleqtrdi compare to eleqtri or eleqtrd
proposed syl6eleqr eleqtrrdi compare to eleqtrri or eleqtrrd
proposed syl6ss sstrdi compare to sstri or sstrd
proposed syl6sseq sseqtrdi compare to sseqtri or sseqtrd
proposed syl6sseqr sseqtrrdi
proposed syl6eqss eqsstrdi compare to eqsstri or eqsstrd
proposed syl6eqssr eqsstrrdi compare to eqsstrri or eqsstrrd
(Please send any comments on these proposals to the mailing list or
Expand All @@ -80,6 +79,7 @@ make a github issue.)
DONE:
Date Old New Notes
23-Jan-24 nelb [same] moved from TA's mathbox to main set.mm
22-Jan-24 syl6sseqr sseqtrrdi
20-Jan-24 nfiund nfiundg
20-Jan-24 bnj1441 bnj1441g
20-Jan-24 cbviinv cbviinvg
Expand Down
46 changes: 23 additions & 23 deletions iset.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27555,11 +27555,11 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
$}

${
syl6ssr.1 $e |- ( ph -> A C_ B ) $.
syl6ssr.2 $e |- C = B $.
sseqtrrdi.1 $e |- ( ph -> A C_ B ) $.
sseqtrrdi.2 $e |- C = B $.
$( A chained subclass and equality deduction. (Contributed by NM,
25-Apr-2004.) $)
syl6sseqr $p |- ( ph -> A C_ C ) $=
sseqtrrdi $p |- ( ph -> A C_ C ) $=
( eqcomi syl6sseq ) ABCDEDCFGH $.
$}

Expand Down Expand Up @@ -38851,7 +38851,7 @@ rather than an implication (but the two are equivalent by ~ bm1.3ii ),
(Contributed by NM, 29-Nov-2003.) $)
iunpw $p |- ( E. x e. A x = U. A <-> ~P U. A = U_ x e. A ~P x ) $=
( vy cuni wceq wrex cpw ciun wcel sseq2 biimprcd reximdv com12 ssiun elpw
cv wss eliun wa uniiun syl6sseqr impbid1 df-pw abeq2i bitri 3bitr4g eqrdv
cv wss eliun wa uniiun sseqtrrdi impbid1 df-pw abeq2i bitri 3bitr4g eqrdv
vex rexbii ssid uniex eleq2 syl5bbr mpbii sylib elssuni elpwi eqss sylibr
anim12i ex reximia syl impbii ) AQZBEZFZABGZVGHZABVFHZIZFZVIDVJVLVIDQZVGR
ZVNVFRZABGZVNVJJVNVLJZVIVOVQVOVIVQVOVHVPABVHVPVOVFVGVNKLMNVQVNABVFIVGABVF
Expand Down Expand Up @@ -45515,7 +45515,7 @@ Definite description binder (inverted iota)
Salmon, 11-Jul-2011.) $)
iotanul $p |- ( -. E! x ph -> ( iota x ph ) = (/) ) $=
( vz weu wn cio c0 wss wceq weq wb wal wex df-eu cab dfiota2 alnex ax-in2
cuni wi alimi ss2ab sylibr dfnul2 syl6sseqr sylbir uni0 syl6sseq eqsstrid
cuni wi alimi ss2ab sylibr dfnul2 sseqtrrdi sylbir uni0 syl6sseq eqsstrid
unissd sylnbi ss0 syl ) ABDZEABFZGHZUOGIUNABCJKBLZCMZUPABCNUREZUOUQCOZSZG
ABCPUSVAGSGUSUTGUSUQEZCLZUTGHUQCQVCUTCCJEZCOZGVCUQVDTZCLUTVEHVBVFCUQVDRUA
UQVDCUBUCCUDUEUFUJUGUHUIUKUOULUM $.
Expand All @@ -45539,7 +45539,7 @@ Definite description binder (inverted iota)
iotass $p |- ( A. x ( ph -> x C_ A ) -> ( iota x ph ) C_ A ) $=
( vy cv wss wal cio cab csn wceq cuni df-iota cpw unieq vex df-pw sspwuni
wi sylib unisn syl6eq sseq2i ss2ab bitri biimpri sseq1 syl2anr ex ss2abdv
biimpa syl6sseqr eqsstrid ) ABECFZSBGZABHABIZDEZJZKZDIZLZCABDMUOUTCNZFVAC
biimpa sseqtrrdi eqsstrid ) ABECFZSBGZABHABIZDEZJZKZDIZLZCABDMUOUTCNZFVAC
FUOUTUQCFZDIVBUOUSVCDUOUSVCUSUPLZUQKZVDCFZVCUOUSVDURLUQUPUROUQDPUAUBUOUPV
BFZVFVGUOVGUPUNBIZFUOVBVHUPBCQUCAUNBUDUEUFUPCRTVEVFVCVDUQCUGUKUHUIUJDCQUL
UTCRTUM $.
Expand Down Expand Up @@ -57858,7 +57858,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) $=
( vz cdm wcel cv wex cfv cres wceq wa con0 wi syl com3l crecs cop ibi wfn
eldm2g wral wrex cab cuni df-recs eleq2i eluniab bitri wss abeq2i elssuni
fnop rspe recsfval syl6sseqr sylbir fveq2 reseq2 fveq2d rspcv fndm eleq2d
fnop rspe recsfval sseqtrrdi sylbir fveq2 reseq2 fveq2d rspcv fndm eleq2d
eqeq12d wfun tfrlem7 funssfv mp3an1 adantrl eleq1d onelss imp31 fun2ssres
syl6bir w3a sylan2 exbiri exp31 com34 com24 sylbird syld imp4d mpdi exp4d
ex com4r pm2.43i imp4a rexlimdv imp exlimiv sylbi ) DFUAZIZJZDHKZUBZWRJZH
Expand Down Expand Up @@ -58010,7 +58010,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
shortened by Mario Carneiro, 24-May-2019.) $)
tfrlemibfn $p |- ( ph -> U. B Fn x ) $=
( wss cvv wcel syl cuni wfun cdm cv wceq wfn crecs tfrlemibacc recsfval
unissd syl6sseqr tfrlem7 funss cxp cpw cfv cop csn cun w3a wex wrex cab
unissd sseqtrrdi tfrlem7 funss cxp cpw cfv cop csn cun w3a wex wrex cab
mpisyl wa simpr3 csuc wf wal ad2antrr con0 simplr onelon syl2anc simpr1
simpr2 tfrlemisucfn dffn2 sylib fssxp word eloni ordsucss sylc xpss1 wb
sstrd vex tfrlem3-2d simprd opexg sylancr snexg unexg mpbird eqeltrd ex
Expand Down Expand Up @@ -58039,7 +58039,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
tfrlemiubacc $p |- ( ph ->
A. u e. x ( U. B ` u ) = ( F ` ( U. B |` u ) ) ) $=
( cfv wceq wcel cv cuni cres wral crecs cdm wfn tfrlemibfn fndm syl wss
tfrlemibacc unissd recsfval syl6sseqr dmss eqsstrrd sselda tfrlem9 wfun
tfrlemibacc unissd recsfval sseqtrrdi dmss eqsstrrd sselda tfrlem9 wfun
wa tfrlem7 a1i adantr eleq2d biimpar funssfv syl3anc word eloni ordelss
sylan sseqtrrd fun2ssres fveq2d 3eqtr3d ralrimiva fveq2 eqeq12d cbvralv
con0 reseq2 sylibr ) AEUAZHUBZRZWEWDUCZLRZSZEBUAZUDFUAZWERZWEWKUCZLRZSZ
Expand Down Expand Up @@ -58107,7 +58107,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
cun wal simprl fneq2 raleq anbi12d rspcev adantll tfrlem3a tfrlemisucaccv
vex sylibr tfrlem3-2d simprd opexg sylancr snidg 3syl wi opeldmg mpd dmeq
elun2 eleq2d syl2anc exlimddv eliun ssrdv cuni recsfval dmeqi dmuni eqtri
ex syl6sseqr eqssd ) AFUAZNZOWPUBWPOUFABCDEFGUCWPUGUDAOIDIPZNZUEZWPAJOWSA
ex sseqtrrdi eqssd ) AFUAZNZOWPUBWPOUFABCDEFGUCWPUGUDAOIDIPZNZUEZWPAJOWSA
JPZOQZWTWSQZAXARZWTWRQZIDUHZXBXCKPZWTUIZLPZXFSXFXHUJFSUKZLWTULZRZXEKABCLD
WTEKFGHUMXCXKRZXFWTXFFSZUNZUOZUSZDQWTXPNZQZXEXLBCJDEKFGAFUPZBPFSTQRBUTXAX
KHUQAXAXKURXCXGXJVAXLXFMPZUIZXILXTULZRZMOUHZXFDQXAXKYDAYCXKMWTOXTWTUKYAXG
Expand Down Expand Up @@ -58229,7 +58229,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
a subset of ` recs ` . (Contributed by Jim Kingdon, 15-Mar-2022.) $)
tfr1onlemssrecs $p |- ( ph -> U. A C_ recs ( G ) ) $=
( cuni cv wfn cfv cres wceq wral wa con0 wrex cab word wss ordsson ssrexv
crecs wi 3syl ss2abdv eqsstrid unissd df-recs syl6sseqr ) ADJEKZBKZLCKZUM
crecs wi 3syl ss2abdv eqsstrid unissd df-recs sseqtrrdi ) ADJEKZBKZLCKZUM
MUMUONFMOCUNPQZBRSZETZJFUEADURADUPBGSZETURHAUSUQEAGUAGRUBUSUQUFIGUCUPBGRU
DUGUHUIUJBCEFUKUL $.
$}
Expand Down Expand Up @@ -58531,7 +58531,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
csuc wi wal 3expia alrimiv fneq1 fveq2 eleq1d imbi12d spv syl rspcdva
ralrimiva imp opexg sylancr snidg elun2 3syl opeldmg mpd dmeq syl2anc
eleq2d exlimddv eliun ssrdv dmuni wss tfr1onlemssrecs eqsstrrid sstrd
ex dmss dmeqi syl6sseqr ) AIGUEZUFZFUFAIUADUARZUFZUGZYBAUBIYEAUBRZISZ
ex dmss dmeqi sseqtrrdi ) AIGUEZUFZFUFAIUADUARZUFZUGZYBAUBIYEAUBRZISZ
YFYESZAYGUHZYFYDSZUADUIZYHYIQRZYFUJZUCRZYLUKYLYNULGUKUMZUCYFUNZUHZYKQ
AYGYFHSZYQQUOYIHUPZYGIHSZUHYRAYSYGLUQYIYGYTAYGURZAYTYGPUQUSYFIHUTVAZA
BCUCDYFEQFGHJKLMNOVBVFYIYQUHZYLYFYLGUKZVCZVDZVEZDSYFUUGUFZSZYKUUCBCUB
Expand Down Expand Up @@ -58926,7 +58926,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
vex fveq1 ralbidv rexbidv elab2 sylibr tfrcllemsucaccv cvv imbi1d wal
3expia alrimiv eleq1d imbi12d spv syl ralrimiva rspcdva opexg sylancr
wi imp snidg elun2 3syl opeldmg dmeq eleq2d syl2anc exlimddv eliun ex
mpd ssrdv dmuni tfrcllemssrecs dmss eqsstrrid sstrd dmeqi syl6sseqr
mpd ssrdv dmuni tfrcllemssrecs dmss eqsstrrid sstrd dmeqi sseqtrrdi
wss ) AJHUEZUFZGUFAJUADUAUNZUFZUGZYJAUBJYMAUBUNZJRZYNYMRZAYOSZYNYLRZU
ADUHZYPYQYNEUCUNZVFZUDUNZYTTZYTUUBUIZHTZUJZUDYNUKZSZYSUCAYOYNIRZUUHUC
ULYQIUMZYOJIRZSUUIAUUJYOMUOYQYOUUKAYOUPZAUUKYOQUOUQYNJIURUSZABCUDDYNE
Expand Down Expand Up @@ -69664,7 +69664,7 @@ elements or fails to hold (is equal to ` (/) ` ) for some element.
cinl csuc elelsuc df-2o eleqtrri a1i ffvelrnd adantr eqeltrrd 0ex djulclb
wf wb orcd df-dc cpr 1oex prid2 df2o3 wrex simp-4r djulcl syl2anc simplrr
foelrn fveq2d simp-5r 3eqtrd elpri eleq2s ad2antrl mpjaodan rexlimddv wne
djune neii pm2.65da olcd syl6sseqr exmidfodomrlemeldju exlimdd ex alrimiv
djune neii pm2.65da olcd sseqtrrdi exmidfodomrlemeldju exlimdd ex alrimiv
simplr df-exmid ) CFZBFZGZCHZYTAFZIJZKZUUCYTDFZUCZDHZLZBUDZAUDZEFZMUEZUFZ
MUULGZUGZLZEUDUHUUKUUQEUUKUUNUUPUUKUUNKZNUULOUAZUUFUCZUUPDUUKUUNDUUJDAUUI
DBUUEUUHDUUEDUIUUGDUJUKULULUUNDUIUMUUPDUIUURUUKYSUUSGZCHZUUSNIJZKZUUTDHZU
Expand Down Expand Up @@ -69708,7 +69708,7 @@ elements or fails to hold (is equal to ` (/) ` ) for some element.
orcd df-dc sylibr simp-4r djulcl foelrn syl2anc simprr wb eqeq1d ad2antlr
wrex fvres mpbird adantr simpr fveq2d simp-5r 3eqtrd elpri df2o3 ad2antrl
cpr eleq2s mpjaodan rexlimddv wne 0ex djune neii a1i mtbiri pm2.65da olcd
eqeq12d simplr syl6sseqr wf 1oex eleqtrri ffvelrnd exmidfodomrlemreseldju
eqeq12d simplr sseqtrrdi wf 1oex eleqtrri ffvelrnd exmidfodomrlemreseldju
fof prid2 csuc elelsuc df-2o exlimdd ex alrimiv df-exmid ) CFZBFZGZCHZUUF
AFZIJZKZUUIUUFDFZUAZDHZLZBUBZAUBZEFZMUDZUEZMUURGZUFZLZEUBUGUUQUVCEUUQUUTU
VBUUQUUTKZNUUROUHZUULUAZUVBDUUQUUTDUUPDAUUODBUUKUUNDUUKDUIUUMDUJUKULULUUT
Expand Down Expand Up @@ -94736,7 +94736,7 @@ nonnegative integers (cont.)". $)
$( The upper integers starting from a natural are a subset of the naturals.
(Contributed by Scott Fenton, 29-Jun-2013.) $)
uznnssnn $p |- ( N e. NN -> ( ZZ>= ` N ) C_ NN ) $=
( cn wcel cuz cfv c1 wss elnnuz uzss sylbi nnuz syl6sseqr ) ABCZADEZFDEZBMA
( cn wcel cuz cfv c1 wss elnnuz uzss sylbi nnuz sseqtrrdi ) ABCZADEZFDEZBMA
OCNOGAHFAIJKL $.

${
Expand Down Expand Up @@ -109818,7 +109818,7 @@ a function (ordinarily on a subset of ` CC ` ) and produces a new
( vz vw cc wcel wa cv cmin co wbr copab cvv cshi wceq caddc wrex sylancom
simpr simpl cdm cab crn cxp wss simplr simpll subcld breldmg mp3an2 npcan
vex eqcomd ancoms adantr oveq1 eqeq2d rspcev syl2anc eqeq1 rexbidv sylibr
elab brelrng jca ssopab2dv df-xp syl6sseqr dmexg abrexexg syl rnexg xpexg
elab brelrng jca ssopab2dv df-xp sseqtrrdi dmexg abrexexg syl rnexg xpexg
expl ssexg syl2an elex breq anbi2d opabbidv breq1d df-shft ovmpog syl3an1
oveq2 syl3anc ) CHIZDEIZJWKWJAKZHIZWLCLMZBKZDNZJZABOZPIZDCQMWRRZWJWKUBWJW
KUCWJWRFKZGKZCSMZRZGDUDZTZFUEZDUFZUGZUHXIPIZWSWKWJWRWLXGIZWOXHIZJZABOXIWJ
Expand Down Expand Up @@ -109872,7 +109872,7 @@ a function (ordinarily on a subset of ` CC ` ) and produces a new
( vz vw cc wcel cv cmin co wbr wa copab cvv cshi wceq caddc wrex sylancom
cdm cab crn cxp wss simplr simpll subcld vex breldmg mp3an2 eqcomd ancoms
npcan adantr oveq1 eqeq2d rspcev syl2anc eqeq1 rexbidv sylibr brelrng jca
elab expl ssopab2dv df-xp syl6sseqr dmex abrexex rnex xpex sylancl anbi2d
elab expl ssopab2dv df-xp sseqtrrdi dmex abrexex rnex xpex sylancl anbi2d
ssexg breq opabbidv oveq2 breq1d df-shft ovmpog mp3an1 mpdan ) CHIZAJZHIZ
WGCKLZBJZDMZNZABOZPIZDCQLWMRZWFWMFJZGJZCSLZRZGDUBZTZFUCZDUDZUEZUFXDPIWNWF
WMWGXBIZWJXCIZNZABOXDWFWLXGABWFWHWKXGWFWHNZWKNZXEXFXIWGWRRZGWTTZXEXIWIWTI
Expand Down Expand Up @@ -133351,7 +133351,7 @@ _Introduction to General Topology_ (1983), p. 114) and it is convenient
$( A member of a topology is a subset of its underlying set. (Contributed
by NM, 12-Sep-2006.) $)
eltopss $p |- ( ( J e. Top /\ A e. J ) -> A C_ X ) $=
( wcel wss ctop cuni elssuni syl6sseqr adantl ) ABEZACFBGELABHCABIDJK $.
( wcel wss ctop cuni elssuni sseqtrrdi adantl ) ABEZACFBGELABHCABIDJK $.
$}


Expand Down Expand Up @@ -134325,7 +134325,7 @@ we show (in ~ tgcl ) that ` ( topGen `` B ) ` is indeed a topology (on
$( The difference of a closed set with an open set is open. (Contributed
by Mario Carneiro, 6-Jan-2014.) $)
difopn $p |- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> ( A \ B ) e. J ) $=
( wcel ccld cfv wa cin cdif wss wceq elssuni syl6sseqr adantr df-ss sylib
( wcel ccld cfv wa cin cdif wss wceq elssuni sseqtrrdi adantr df-ss sylib
cuni adantl difeq1d indif2 cldrcl simpl cldopn syl3anc eqeltrrid eqeltrrd
ctop inopn ) ACFZBCGHFZIZADJZBKZABKCUMUNABUMADLZUNAMUKUPULUKACSDACNEOPADQ
RUAUMUOADBKZJZCADBUBUMCUIFZUKUQCFZURCFULUSUKBCUCTUKULUDULUTUKBCDEUETAUQCU
Expand Down Expand Up @@ -134948,7 +134948,7 @@ we show (in ~ tgcl ) that ` ( topGen `` B ) ` is indeed a topology (on
( topGen ` ( B |`t A ) ) = ( ( topGen ` B ) |`t A ) ) $=
( vx vy vz vw wcel wa crest cv wss cuni wceq wex cvv cin cmpt crn ctg cfv
co wb cxp wfn restfn elex fnovex mp3an3an syl cima wfun simpll funmpt a1i
eltg3 restval sseq2d wral vex inex1 rgenw eqid fnmpt fnima mp2b syl6sseqr
eltg3 restval sseq2d wral vex inex1 rgenw eqid fnmpt fnima mp2b sseqtrrdi
biimpa ssimaexg syl3anc wi ciun df-ima resmpt adantl syl5eq unieqd dfiun3
cres rneqd syl6eqr iunin1 syl6eq tgvalex ad2antrr adantr uniiun eqeltrrid
simpr eltg3i adantlr elrestr eqeltrd unieq syl5ibrcom expimpd exlimdv mpd
Expand Down Expand Up @@ -136388,7 +136388,7 @@ F C_ ( CC X. X ) ) $=
( vz vr vs cxp cv wcel wa wrex wss wceq vw cuni relxp cop eleq2i eluni2
bitri anbi12i opelxp reeanv 3bitr4i eqid xpeq1 eqeq2d xpeq2 rspc2ev vex
mp3an3 xpex eqeq1 2rexbidv crn cab rnmpo eqtri elab2 sylibr elssuni syl
cmpo sseld syl5bir rexlimivv relssi cpw wf wral syl6sseqr xpss12 syl2an
cmpo sseld syl5bir rexlimivv relssi cpw wf wral sseqtrrdi xpss12 syl2an
sylbi elpw rgen2 fmpo mpbi frn ax-mp eqsstri sspwuni eqssi ) FGNZCUBZKU
AWKWLFGUCKOZUAOZUDZWKPZWMLOZPZWNMOZPZQZMERLDRZWOWLPZWMFPZWNGPZQWRLDRZWT
MERZQWPXBXDXFXEXGXDWMDUBZPXFFXHWMIUELWMDUFUGXEWNEUBZPXGGXIWNJUEMWNEUFUG
Expand Down Expand Up @@ -140719,7 +140719,7 @@ S C_ ( P ( ball ` D ) T ) ) $=
tgioo $p |- ( topGen ` ran (,) ) = J $=
( vz cioo cr wcel wceq wss cv co wa c1 cxr syl2anc syl clt cmnf wbr cbl
vv vx vy va vb cfv crn ctg cxmet rexmet mopnval ax-mp blex rnex blssioo
vw cvv crp wrex wral cuni elssuni unirnioo syl6sseqr cin retopbas simpl
vw cvv crp wrex wral cuni elssuni unirnioo sseqtrrdi cin retopbas simpl
ctb a1i sselda cmin caddc 1re bl2ioo mpan2 peano2rem peano2re ioorebasg
rexrd eqeltrd simpr 1rp blcntr mp3an13 elind basis2 syl22anc cxp cpw wf
wfn wb ioof ffn ovelrn mp2b wi eleq2 sseq1 anbi12d csup cinf inss2 sstr
Expand Down
Loading

0 comments on commit 4d51170

Please sign in to comment.