Skip to content

Commit

Permalink
Rename syl6breq to breqtrdi (metamath#3722)
Browse files Browse the repository at this point in the history 
This is in set.mm and iset.mm.
  • Loading branch information
@jkingdon
jkingdon authored Dec 29, 2023
1 parent 380eecb commit 0064381
Show file tree
Hide file tree
Showing 3 changed files with 154 additions and 154 deletions.
2 changes: 1 addition & 1 deletion changes-set.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,12 +78,12 @@ proposed syl6eqss eqsstrdi compare to eqsstri or eqsstrd
proposed syl6eqssr eqsstrrdi compare to eqsstrri or eqsstrrd
proposed syl6eqbr eqbrtrdi compare to eqbrtri or eqbrtrd
proposed syl6eqbrr eqbrtrrdi compare to eqbrtrri or eqbrtrrd
proposed syl6breq breqtrdi compare to breqtri or breqtrd
(Please send any comments on these proposals to the mailing list or
make a github issue.)

DONE:
Date Old New Notes
28-Dec-23 syl6breq breqtrdi compare to breqtri or breqtrd
26-Dec-23 syl6breqr breqtrrdi compare to breqtrri or breqtrrd
25-Dec-23 prth anim12
25-Dec-23 selpw velpw
Expand Down
30 changes: 15 additions & 15 deletions iset.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34340,11 +34340,11 @@ same disjoint variable group (meaning ` A ` cannot depend on ` x ` ) and
$}

${
syl6breq.1 $e |- ( ph -> A R B ) $.
syl6breq.2 $e |- B = C $.
breqtrdi.1 $e |- ( ph -> A R B ) $.
breqtrdi.2 $e |- B = C $.
$( A chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.) $)
syl6breq $p |- ( ph -> A R C ) $=
breqtrdi $p |- ( ph -> A R C ) $=
( eqid 3brtr3g ) ABCBDEFBHGI $.
$}

Expand All @@ -34354,7 +34354,7 @@ same disjoint variable group (meaning ` A ` cannot depend on ` x ` ) and
$( A chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.) $)
breqtrrdi $p |- ( ph -> A R C ) $=
( eqcomi syl6breq ) ABCDEFDCGHI $.
( eqcomi breqtrdi ) ABCDEFDCGHI $.
$}

${
Expand Down Expand Up @@ -69327,7 +69327,7 @@ elements or fails to hold (is equal to ` (/) ` ) for some element.
and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.) $)
en2eleq $p |- ( ( X e. P /\ P ~~ 2o ) -> P = { X , U. ( P \ { X } ) } ) $=
( wcel c2o cen wbr csn cdif cuni wne cpr wceq c1o com csuc 1onn simpr df-2o
wa syl6breq simpl dif1en mp3an2i en1uniel syl sylib simprd necomd wi simpld
wa breqtrdi simpl dif1en mp3an2i en1uniel syl sylib simprd necomd wi simpld
eldifsn en2eqpr syl3anc mpd ) BACZADEFZSZBABGHZIZJZABUSKLZUQUSBUQUSACZUSBJZ
UQUSURCZVBVCSUQURMEFZVDMNCUQAMOZEFUOVEPUQADVFEUOUPQZRTUOUPUAZAMBUBUCURUDUEU
SABUKUFZUGUHUQUPUOVBUTVAUIVGVHUQVBVCVIUJBUSAULUMUN $.
Expand All @@ -69337,7 +69337,7 @@ elements or fails to hold (is equal to ` (/) ` ) for some element.
en2other2 $p |- ( ( X e. P /\ P ~~ 2o ) ->
U. ( P \ { U. ( P \ { X } ) } ) = X ) $=
( wcel c2o cen wbr csn cdif cuni cpr en2eleq prcom syl6eq difeq1d difprsnss
wa syl6eqss wne simpl c1o com csuc 1onn simpr df-2o syl6breq dif1en syl3anc
wa syl6eqss wne simpl c1o com csuc 1onn simpr df-2o breqtrdi dif1en syl3anc
a1i en1uniel eldifsni 3syl necomd eldifsn sylanbrc snssd unieqd wceq unisng
eqssd adantr eqtrd ) BACZADEFZPZAABGZHZIZGZHZIVFIZBVEVJVFVEVJVFVEVJVHBJZVIH
VFVEAVLVIVEABVHJVLABKBVHLMNVHBOQVEBVJVEVCBVHRBVJCVCVDSZVEVHBVEVGTEFZVHVGCVH
Expand Down Expand Up @@ -69673,7 +69673,7 @@ Similar to the Axiom of Choice (first form) of [Enderton] p. 49.
of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.)
(Revised by Mario Carneiro, 29-Apr-2015.) $)
dju0en $p |- ( A e. V -> ( A |_| (/) ) ~~ A ) $=
( wcel cdju cun cen cvv cin wceq wbr 0ex in0 endjudisj mp3an23 un0 syl6breq
( wcel cdju cun cen cvv cin wceq wbr 0ex in0 endjudisj mp3an23 un0 breqtrdi
c0 ) ABCZAQDZAQEZAFRQGCAQHQISTFJKALAQBGMNAOP $.

$( Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258.
Expand Down Expand Up @@ -113291,7 +113291,7 @@ A Cauchy sequence (as defined here, which has a rate of convergence
$( The maximum of two reals is no smaller than the second real. Lemma 3.10
of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.) $)
maxle2 $p |- ( ( A e. RR /\ B e. RR ) -> B <_ sup ( { A , B } , RR , < ) ) $=
( cr wcel wa cpr clt csup cle wbr maxle1 ancoms maxcom syl6breq ) ACDZBCDZE
( cr wcel wa cpr clt csup cle wbr maxle1 ancoms maxcom breqtrdi ) ACDZBCDZE
BBAFCGHZABFCGHIPOBQIJBAKLBAMN $.

${
Expand Down Expand Up @@ -113951,7 +113951,7 @@ A Cauchy sequence (as defined here, which has a rate of convergence
30-Apr-2023.) $)
xrmax2sup $p |- ( ( A e. RR* /\ B e. RR* )
-> B <_ sup ( { A , B } , RR* , < ) ) $=
( cxr wcel wa cpr clt csup cle wbr xrmax1sup ancoms prcom supeq1i syl6breq
( cxr wcel wa cpr clt csup cle wbr xrmax1sup ancoms prcom supeq1i breqtrdi
) ACDZBCDZEBBAFZCGHZABFZCGHIQPBSIJBAKLCRTGBAMNO $.

$( The maximum of two real numbers is the same when taken as extended reals
Expand Down Expand Up @@ -120308,7 +120308,7 @@ Infinite sums (cont.)
rexbidv elab2g mpbird letrd nn0ex mptex biimpri syl2an2 readdcl seq3feq
1nn0 recnd serf0 climi0 fveq2i oveq1i oveq2i breq2i ralbii sylib absidd
cbvsumv sumeq2i rspccva nfv nfsum1 nfbr cbvral syl6bbr eqeltrrid biimpi
syl6breq csb nfcsb1v nfeq2 csbeq1a nfel1 eqeq2i abbii mertenslemi1 expr
breqtrdi csb nfcsb1v nfeq2 csbeq1a nfel1 eqeq2i abbii mertenslemi1 expr
eqtri ex syl5bir expdimp ) AJULZUMNUNUOZUPZUQFIURZUSUTVAUPZLUUMVBUTZUQH
ULZPUPZHURZVFUMUTZVBUTZVCVDZJQULZVGUPZVEZQVHVIUNUYIVJUTZEUYIUYOUSUTVFUM
UTVGUPFIURVKUTHURVAUPLVCVDJCULZVGUPVECUQVIZAUYLUYKUYSQJUYJVFVHVLAVMZAUY
Expand Down Expand Up @@ -120756,7 +120756,7 @@ Infinite sums (cont.)
eqtr4i df-e breqtrrdi cn clt nnred nngt0d 1re 0le1 divge0 mpanl12 syl2anc
breqtrrd climserle eqbrtrrd mptru cmin nnuz 1zzd recnd 0p1e1 seqeq1 ax-mp
clim2ser oveq2i 3brtr3g cmul 2cnd halfre id reexpcld eqid reexpcl sylancr
oveq2 simpr cabs 1lt2 mp2an breqtrri 2m1e1 eqtri syl6breq sylan2 nnrpd
oveq2 simpr cabs 1lt2 mp2an breqtrri 2m1e1 eqtri breqtrdi sylan2 nnrpd
2re 0le2 absid georeclim 2cn halfcn exp0 eqeltri nnnn0 remulcld isermulc2
eqtr4d 2t1e2 remulcl faclbnd2 nnexpcl rphalfcld lerecd mpbid nncnd nnap0d
2nn divrecapd cap 2ap0 recdivapd exprecapd 3eqtr4rd 3brtr4d ere lesubaddi
Expand Down Expand Up @@ -122139,7 +122139,7 @@ Infinite sums (cont.)
cioc cexp cmin ccos cfv wceq cxr w3a 0xr elioc2 mp2an simp1bi resqcld recnd
cap 2cn 3cn pm3.2i div12ap mp3an13 syl cz 2z expgt0 3adant3 sylbi 2lt3 3pos
mp3an2 ltdiv1ii dividapi breqtri redivclapi mp3an12 syl2anc mulid1d breqtrd
mpbi ltmul2 mpbii eqbrtrd wi 0re ltle mpan imdistani le2sq2 mpanr1 syl6breq
mpbi ltmul2 mpbii eqbrtrd wi 0re ltle mpan imdistani le2sq2 mpanr1 breqtrdi
stoic3 redivclap mp3an23 remulcl sylancr ltletr mp3an3 mp2and sylancl mpbid
sq1 posdif cos01bnd simpld resubcl recoscld lttr mp3an2i ) ABCUADEZBCFAFUBD
ZGHDZIDZUCDZJKZXLAUDUEZJKZBXNJKZXHXKCJKZXMXHXKXIJKZXICLKZXQXHXKXIFGHDZIDZXI
Expand All @@ -122158,7 +122158,7 @@ Infinite sums (cont.)
( cc0 c2 cioc co wcel cmul csin cfv clt cr wbr cle wb 2re syl c1 wa 2pos cc
cdiv ccos w3a cxr 0xr elioc2 mp2an rehalfcl 3ad2ant1 sylbi resincl remulcld
recoscl divgt0 mpanr12 3adant3 pm3.2i lediv1 mp3an23 biimpa 2div2e1 3adant2
syl6breq 3jca 1re 3imtr4i sin01gt0 cos01gt0 wi axmulgt0 syl2anc mp2and mpan
breqtrdi 3jca 1re 3imtr4i sin01gt0 cos01gt0 wi axmulgt0 syl2anc mp2and mpan
mpani sylc wceq recnd sin2t breqtrrd simp1bi cap 2cn 2ap0 divcanap2 breqtrd
fveq2d ) ABCDEFZBCACUAEZGEZHIZAHIJWGBCWHHIZWHUBIZGEZGEZWJJWGWMKFZBWMJLZBWNJ
LZWGWHKFZWOWGAKFZBAJLZACMLZUCZWRBUDFZCKFZWGXBNUEOBCAUFUGZWSWTWRXAAUHUIZUJZW
Expand Down Expand Up @@ -129234,7 +129234,7 @@ reduced fraction representation (no common factors, denominator
( vz cn cen wbr cin c0 wceq cun c2 wn crab ensymi entr mpan2 wa wo wcel
cz w3a cv cdvds oddennn 3ad2ant1 evenennn 3ad2ant2 simp3 inrab wral ancom
pm3.24 mtbi rgenw rabeq0 mpbir eqtri a1i syl22anc unrab rabid2 wdc nnz 2z
unen zdvdsdc mpan exmiddc 3syl orcomd mprgbir eqtr4i syl6breq ) ADEFZBDEF
unen zdvdsdc mpan exmiddc 3syl orcomd mprgbir eqtr4i breqtrdi ) ADEFZBDEF
ZABGHIZUAZABJZKCUBZUCFZLZCDMZVTCDMZJZDEVQAWBEFZBWCEFZVPWBWCGZHIZVRWDEFVNV
OWEVPVNDWBEFWEWBDCUDNADWBOPUEVOVNWFVPVODWCEFWFWCDCUFNBDWCOPUGVNVOVPUHWHVQ
WGWAVTQZCDMZHWAVTCDUIWJHIWILZCDUJWKCDVTWAQWIVTULVTWAUKUMUNWICDUOUPUQURAWB
Expand Down Expand Up @@ -148186,7 +148186,7 @@ Limited Principle of Omniscience (LPO) implies excluded middle, so we
eqeltrd iserex mpbid isumrecl cvv wbr seqex ax-1cn geo2lim ax-mp adantr
cle eqbrtrd wo elpri breqtrrd breldmg mp3an rpge0d mulid1d leidd fsumle
mpjaodan rpgt0d leltaddd trilpolemisumle ltleaddd eqbrtrid ltned neneqd
geoihalfsum syl6breq pm2.65da ffvelrnda orcomd ecased ralrimiva ) ABUAZ
geoihalfsum breqtrdi pm2.65da ffvelrnda orcomd ecased ralrimiva ) ABUAZ
EJZKUDZBLAUVBLMZVJZUVDUVCNUDZUVFUVGCKUDZAUVHUVEUVGHUBUVFUVGVJZCKUVICKAC
OMUVEUVGACDEFGUCUBUVICLKPDUAZUEQZUFQZDRZKUGUVICKUVBUHQZUVLDRZUVBKSQZUIJ
ZUVLDRZSQZUVMUGUVICKUVBUJQZUVBUKULZUVLDRZUVRSQZUVSUGUVICUVTUVLDRZKPUVBU
Expand Down
Loading

0 comments on commit 0064381

Please sign in to comment.