Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rename sseqtr4d to sseqtrrd #3772

Merged
merged 1 commit into from
Jan 17, 2024
Merged

Rename sseqtr4d to sseqtrrd #3772

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion changes-set.txt
View file
Open in desktop
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 sseqtr4d sseqtrrd
proposed syl6sseqr sseqtrrdi
proposed syl6eqss eqsstrdi compare to eqsstri or eqsstrd
proposed syl6eqssr eqsstrrdi compare to eqsstrri or eqsstrrd
Expand All @@ -80,6 +79,7 @@ make a github issue.)

DONE:
Date Old New Notes
15-Jan-24 sseqtr4d sseqtrrd
14-Jan-24 sseqtr4i sseqtrri
5-Jan-24 --- --- sections "Groups" and "Simple groups"
moved from RR's mathbox to main set.mm
Expand Down
58 changes: 29 additions & 29 deletions iset.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27369,11 +27369,11 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
$}

${
sseqtr4d.1 $e |- ( ph -> A C_ B ) $.
sseqtr4d.2 $e |- ( ph -> C = B ) $.
sseqtrrd.1 $e |- ( ph -> A C_ B ) $.
sseqtrrd.2 $e |- ( ph -> C = B ) $.
$( Substitution of equality into a subclass relationship. (Contributed by
NM, 25-Apr-2004.) $)
sseqtr4d $p |- ( ph -> A C_ C ) $=
sseqtrrd $p |- ( ph -> A C_ C ) $=
( eqcomd sseqtrd ) ABCDEADCFGH $.
$}

Expand Down Expand Up @@ -27492,7 +27492,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
$( Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim,
3-Jun-2011.) $)
sseqtrrid $p |- ( ph -> B C_ C ) $=
( wss a1i sseqtr4d ) ACBDCBGAEHFI $.
( wss a1i sseqtrrd ) ACBDCBGAEHFI $.
$}

${
Expand Down Expand Up @@ -50745,7 +50745,7 @@ We use their notation ("onto" under the arrow). (Contributed by NM,
that set, using the ` Fn ` abbreviation. (Contributed by Stefan O'Rear,
10-Mar-2015.) $)
fnfvima $p |- ( ( F Fn A /\ S C_ A /\ X e. S ) -> ( F ` X ) e. ( F " S ) ) $=
( wfn wss wcel w3a wfun cdm wa cima fnfun 3ad2ant1 simp2 wceq fndm sseqtr4d
( wfn wss wcel w3a wfun cdm wa cima fnfun 3ad2ant1 simp2 wceq fndm sseqtrrd
cfv jca simp3 funfvima2 sylc ) CAEZBAFZDBGZHZCIZBCJZFZKUFDCSCBLGUGUHUJUDUEU
HUFACMNUGBAUIUDUEUFOUDUEUIAPUFACQNRTUDUEUFUABDCUBUC $.

Expand Down Expand Up @@ -57955,7 +57955,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
( cfv wceq wcel cv cuni cres wral crecs cdm wfn tfrlemibfn fndm syl wss
tfrlemibacc unissd recsfval syl6sseqr dmss eqsstrrd sselda tfrlem9 wfun
wa tfrlem7 a1i adantr eleq2d biimpar funssfv syl3anc word eloni ordelss
sylan sseqtr4d fun2ssres fveq2d 3eqtr3d ralrimiva fveq2 eqeq12d cbvralv
sylan sseqtrrd fun2ssres fveq2d 3eqtr3d ralrimiva fveq2 eqeq12d cbvralv
con0 reseq2 sylibr ) AEUAZHUBZRZWEWDUCZLRZSZEBUAZUDFUAZWERZWEWKUCZLRZSZ
FWJUDAWIEWJAWDWJTZVAZWDLUEZRZWRWDUCZLRZWFWHWQWDWRUFZTWSXASAWJXBWDAWJWEU
FZXBAWEWJUGXCWJSZABCDEGHIJKLMNOPQUHWJWEUIUJZAWEWRUKZXCXBUKAWEGUBWRAHGAB
Expand Down Expand Up @@ -58338,7 +58338,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
( cv cuni cfv cres wceq wral wcel wa crecs cdm wfn tfr1onlembfn syl
fndm wss tfr1onlembacc unissd tfr1onlemssrecs sstrd eqsstrrd sselda
dmss con0 wrex eqid tfrlem9 tfrfun eleq2d biimpar funssfv mp3an2ani
cab wfun word ordelon syl2anc eloni sylan adantr sseqtr4d fun2ssres
cab wfun word ordelon syl2anc eloni sylan adantr sseqtrrd fun2ssres
ordelss fveq2d 3eqtr3d ralrimiva reseq2 eqeq12d cbvralv sylibr
fveq2 ) AEUEZHUFZUGZWPWOUHZNUGZUIZEIUJFUEZWPUGZWPXAUHZNUGZUIZFIUJAW
TEIAWOIUKZULZWONUMZUGZXHWOUHZNUGZWQWSXGWOXHUNZUKXIXKUIAIXLWOAIWPUNZ
Expand Down Expand Up @@ -58729,7 +58729,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
( vv vt ve cv cuni cfv cres wceq wral wcel wa crecs cdm tfrcllembfn
wf fdm syl wss tfrcllembacc unissd tfrcllemssrecs sstrd dmss sselda
eqsstrrd wfn con0 wrex cab eqid tfrlem9 wfun tfrfun biimpar funssfv
eleq2d mp3an2ani word ordelon syl2anc eloni ordelss adantr sseqtr4d
eleq2d mp3an2ani word ordelon syl2anc eloni ordelss adantr sseqtrrd
sylan fun2ssres fveq2d 3eqtr3d fveq2 reseq2 eqeq12d cbvralv sylibr
ralrimiva ) AEUIZHUJZUKZXAWTULZOUKZUMZEIUNFUIZXAUKZXAXFULZOUKZUMZFI
UNAXEEIAWTIUOZUPZWTOUQZUKZXMWTULZOUKZXBXDXLWTXMURZUOXNXPUMAIXQWTAIX
Expand Down Expand Up @@ -59173,7 +59173,7 @@ defined for all sets (being defined for all ordinals might be enough if
( A u. U_ x e. B ( F ` ( ( rec ( F , A ) |` B ) ` x ) ) ) ) $=
( vg vy cvv wfn wcel con0 cfv cv cdm ciun cun wceq wa wfun wss w3a tfri2d
crdg cres cmpt df-irdg rdgruledefgg alrimiv 3impa eqidd 3ad2ant3 rdgifnon
dmeq onss fndm syl 3adant3 sseqtr4d ssdmres sylib sylan9eqr fveq2d adantl
dmeq onss fndm syl 3adant3 sseqtrrd ssdmres sylib sylan9eqr fveq2d adantl
fveq1 iuneq12d uneq2d rdgfun resfunexg mpan simpr fvexg sylancl ralrimivw
wral vex wi funfvex funfni ex ralimdv adantr iunexg syl2anc 3adant2 unexg
mpd 3ad2ant2 fvmptd eqtrd ) DHIZBEJZCKJZUAZCDBUCZLZWNCUDZFHBAFMZNZAMZWQLZ
Expand Down Expand Up @@ -69088,7 +69088,7 @@ elements or fails to hold (is equal to ` (/) ` ) for some element.
cmpt cmap co csuc wral xnninf 1oex sucid df-2o eleqtrri 2on0 2onn nn0eln0
wf wne ax-mp mpbir nndcel ancoms ifcldcd eqid fmptd elexi elmap sylibr wn
omex ssid iftrue sseq1d mpbiri iffalse wo peano2 syl2anc exmiddc mpjaodan
0ss simpl adantr sseqtr4d wi wtr word nnord ordtr trsuc sylan ex con3dimp
0ss simpl adantr sseqtrrd wi wtr word nnord ordtr trsuc sylan ex con3dimp
3sstr4d eleq1 ifbid fvmptg simpr ralrimiva fveq1 sseq12d ralbidv df-nninf
elrab2 sylanbrc ) BEFZAEAGZBFZHIJZUAZKEUBUCZFZCGZUDZXGLZXJXGLZMZCEUEZXGUF
FXCEKXGUNXIXCAEXFKXGXCXDEFZNZXEHIKHKFZXQHHUDKHUGUHUIUJZOIKFZXQXTKIUOZUKKE
Expand Down Expand Up @@ -128997,7 +128997,7 @@ reduced fraction representation (no common factors, denominator
sylib cn cuz wo cv elnn1uz2 csn phi1 0z hashsng ax-mp rabid2 elsni oveq1d
syl6eq mprgbir fveq2i 3eqtr2i fveq2 oveq2 eqeq1d rabeqbidv fveq2d 3eqtr4a
gcd1 fzo01 cfz eluz2nn phival fzossfz a1i sseqin2 fzo0ss1 syl6eqr rabeqdv
mpbi inrab2 3eqtr4g cmin phibndlem eluzelz fzoval sseqtr4d df-ss wi wa wn
mpbi inrab2 3eqtr4g cmin phibndlem eluzelz fzoval sseqtrrd df-ss wi wa wn
wral cabs gcd0id eluzelre eluzge2nn0 nn0ge0d absidd eqtrd eluz2b3 simprbi
eqnetrd adantr eleq2s neeq1d syl5ibrcom necon2bd 1z fzospliti sylancl ord
simpr syld ralrimiva rabss sylibr 3eqtr3d jaoi sylbi ) BUACZBDEZBFUBGCZUC
Expand Down Expand Up @@ -130339,7 +130339,7 @@ then the Limited Principle of Omniscience (LPO) implies excluded middle.
syl dcbid cbvralv sylib simpl3 wss wf fof crn imassrn frn sstrid ad2antrr
3adantl1 simpl2 equequ2 cbvral2v ssralv ralimdv sylsyld syl5bi sylc simpr
cfn cres wfun cdm fofun word ordom ordtr ax-mp trss mpsyl wceq fdmd fores
wtr sseqtr4d syl2anc vex resex foeq1 spcev foeq2 exbidv fidcenum sylanbrc
wtr sseqtrrd syl2anc vex resex foeq1 spcev foeq2 exbidv fidcenum sylanbrc
rspcev inffinp1 simprl syl2an2r eqneltrrd ex reximdva rexlimddv ralrimiva
foelrn simprr jca 3com23 3expia impbii ) CUALMZABNZOZBCPZACPZQCDRZUBZDUCZ
QCUEMZUDZYMYQYTUUAYMYQYSERZYRUFZYRFRZUGZSUHZEQUIZFQPZTZDUCZABCDEFUJZUKYMU
Expand Down Expand Up @@ -132888,7 +132888,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
Mario Carneiro, 21-Aug-2015.) $)
toponss $p |- ( ( J e. ( TopOn ` X ) /\ A e. J ) -> A C_ X ) $=
( ctopon cfv wcel wa cuni wss elssuni adantl wceq toponuni adantr sseqtr4d
( ctopon cfv wcel wa cuni wss elssuni adantl wceq toponuni adantr sseqtrrd
) BCDEFZABFZGABHZCQARIPABJKPCRLQCBMNO $.

$( If ` K ` is a topology on the base set of topology ` J ` , then ` J ` is a
Expand Down Expand Up @@ -133865,7 +133865,7 @@ we show (in ~ tgcl ) that ` ( topGen `` B ) ` is indeed a topology (on
ssntr $p |- ( ( ( J e. Top /\ S C_ X ) /\ ( O e. J /\ O C_ S ) ) -> O C_ (
( int ` J ) ` S ) ) $=
( ctop wcel wss wa cpw cin cuni cnt cfv elin elpwg pm5.32i bitr2i elssuni
sylbi adantl wceq ntrval adantr sseqtr4d ) BFGADHIZCBGZCAHZIZICBAJZKZLZAB
sylbi adantl wceq ntrval adantr sseqtrrd ) BFGADHIZCBGZCAHZIZICBAJZKZLZAB
MNNZUICULHZUFUICUKGZUNUOUGCUJGZIUICBUJOUGUPUHCABPQRCUKSTUAUFUMULUBUIABDEU
CUDUE $.

Expand Down Expand Up @@ -134776,7 +134776,7 @@ converges to zero (in the standard topology on the reals) with this
( ( F ` P ) e. y -> E. x e. J ( P e. x /\ x C_ ( `' F " y ) ) ) ) ) ) $=
( ctopon cfv wcel cv cima wss wa wrex wi wral wb ad2antlr ccnp co wf ccnv
w3a iscnp wfun cdm ffun toponss adantlr wceq fdm funimass3 syl2anc anbi2d
sseqtr4d rexbidva imbi2d ralbidv pm5.32da 3ad2ant1 bitrd ) EGIJKZFHIJKZCG
sseqtrrd rexbidva imbi2d ralbidv pm5.32da 3ad2ant1 bitrd ) EGIJKZFHIJKZCG
KZUEDCEFUAUBJKGHDUCZCDJBLZKZCALZKZDVJMVHNZOZAEPZQZBFRZOZVGVIVKVJDUDVHMNZO
ZAEPZQZBFRZOZABCDEFGHUFVDVEVQWCSVFVDVGVPWBVDVGOZVOWABFWDVNVTVIWDVMVSAEWDV
JEKZOZVLVRVKWFDUGZVJDUHZNVLVRSVGWGVDWEGHDUITWFVJGWHVDWEVJGNVGVJEGUJUKVGWH
Expand Down Expand Up @@ -134811,7 +134811,7 @@ converges to zero (in the standard topology on the reals) with this
( vx vf vy vg vj vk cfv wcel ctop co cuni cv cmap cvv wceq ctopon w3a cdm
ccnp cima wa wrex wi wral crab cmpt topontop 3ad2ant1 simp2 uniexg mptexg
wss unieq oveq2d rexeq imbi2d ralbidv rabeqbidv mpteq12dv oveq1d mpteq2dv
raleq df-cnp ovmpog syl3anc dmeqd eqid dmmptss syl6eqss toponuni sseqtr4d
raleq df-cnp ovmpog syl3anc dmeqd eqid dmmptss syl6eqss toponuni sseqtrrd
syl wrel mptrel releqd mpbiri simp3 relelfvdm syl2anc sseldd ) CEUALZMZDN
MZBACDUDOZLMZUBZWIUCZEAWKWLCPZEWKWLFWMFQZGQZLHQZMZWNIQZMWOWRUEWPUQUFZICUG
ZUHZHDUIZGDPZWMROZUJZUKZUCWMWKWIXFWKCNMZWHXFSMZWIXFTWGWHXGWJECULUMWGWHWJU
Expand Down Expand Up @@ -134843,7 +134843,7 @@ converges to zero (in the standard topology on the reals) with this
tgcn $p |- ( ph -> ( F e. ( J Cn K ) <->
( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) ) $=
( vx vz wcel cv wral wa wi ctop syl ccn co wf ccnv cima ctopon wb syl2anc
cfv iscn wss ctg ctb topontop eqeltrrd tgclb sylibr bastg sseqtr4d ssralv
cfv iscn wss ctg ctb topontop eqeltrrd tgclb sylibr bastg sseqtrrd ssralv
cuni wceq wex eleq2d eltg3 bitrd ciun iunopn sylan9r imaeq2 imauni syl6eq
eleq1d imbi2d syl5ibrcom expimpd exlimdv sylbid imp cbvralv syl6ib impbid
ex ralrimdva anbi2d ) ADEFUAUBNZGHDUCZDUDZBOZUEZENZBFPZQZWGWKBCPZQAEGUFUI
Expand All @@ -134862,7 +134862,7 @@ converges to zero (in the standard topology on the reals) with this
( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. B
( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) ) $=
( cfv wcel wss wa wi syl vz ccnp co wf cv cima wrex wral wb iscnp syl3anc
ctopon ctg ctb ctop topontop eqeltrrd tgclb sylibr sseqtr4d ssralv anim2d
ctopon ctg ctb ctop topontop eqeltrrd tgclb sylibr sseqtrrd ssralv anim2d
bastg sylbid eleq2d biimpa tg2 r19.29 sstr expcom reximdv com12 rexlimivw
imim2i imp32 ex com23 ralrimdva sylibrd impbid ) AFEGHUBUCOPZIJFUDZEFOZCU
EZPZEBUEZPZFWFUFZWDQZRZBGUGZSZCDUHZRZAWAWBWLCHUHZRZWNAGIULOPZHJULOPZEIPZW
Expand All @@ -134884,7 +134884,7 @@ converges to zero (in the standard topology on the reals) with this
( ( _I |` X ) e. ( J Cn K ) <-> K C_ J ) ) $=
( vx ctopon cfv wcel wa cid cres ccn co ccnv cv cima wral wf syl6bbr wceq
wss iscn wf1o f1oi f1of biantrur cnvresid imaeq1i elssuni adantl toponuni
ax-mp cuni ad2antlr sseqtr4d resiima syl5eq eleq1d ralbidva dfss3 bitrd
ax-mp cuni ad2antlr sseqtrrd resiima syl5eq eleq1d ralbidva dfss3 bitrd
syl ) ACEFZGZBVBGZHZICJZABKLGZVFMZDNZOZAGZDBPZBATZVEVGCCVFQZVLHVLDVFABCCU
AVNVLCCVFUBVNCUCCCVFUDUKUERVEVLVIAGZDBPVMVEVKVODBVEVIBGZHZVJVIAVQVJVFVIOZ
VIVHVFVICUFUGVQVICTVRVISVQVIBULZCVPVIVSTVEVIBUHUIVDCVSSVCVPCBUJUMUNCVIUOV
Expand Down Expand Up @@ -135270,7 +135270,7 @@ converges to zero (in the standard topology on the reals) with this
ad2antrr jca simprl wrex cdm cnvimass fdm sseqtrid ssralv simp-4l simp-4r
ctop topontop cnprcl2k syl3anc simpllr wfn ffn ad2antlr elpreima simplbda
simprr syl2anc icnpimaex syl33anc wfun ffund toponss sylan fdmd funimass3
wi sseqtr4d anbi2d rexbidva mpbid expr ralimdva syld impr an32s ad3antrrr
wi sseqtrrd anbi2d rexbidva mpbid expr ralimdva syld impr an32s ad3antrrr
eltop2 adantr mpbir2and impbida ) CEIJKZDFIJKZLZBCDUCMKZEFBUDZBANZCDUAMJK
ZAEOZLZXCXDLZXEXHXCXDXEBUBGNZPZCKZGDOZGBCDEFUEZUFXJXHXGACUGZOZXDXQXCXDXGA
XPXFBCDXPXPUHUIQUJXJXGAEXPXAEXPUKXBXDECULUOUMUNUPXCXILZXDXEXNXCXEXHUQXRXM
Expand Down Expand Up @@ -136060,7 +136060,7 @@ F C_ ( CC X. X ) ) $=
cvv nfeq fveq2 eqeq12d rspc sylc eleq1d adantr ad2antrr simplrl icnpimaex
simprl simplrr simprr jca ex opelxp reeanv 3imtr4g sylbid cin an4 biimpri
syl33anc elin a1i simpl toponss syl2an ssinss1 adantl sselda elin1d ffund
wfun cdm fdmd sseqtr4d sseldd funfvima mpd elin2d funimass4 mpbird syldan
wfun cdm fdmd sseqtrrd sseldd funfvima mpd elin2d funimass4 mpbird syldan
eqeltrd adantlr xpss12 sstr2 syl2im anim12d ctop topontop syl inopn 3expb
syl5bi sylan eleq2 vex jctild expimpd imaeq2 sseq1d rspcev syl6 rexlimdvv
anbi12d expd syld ralrimivva rgen2w sseq2 anbi2d rexbidv imbi12d ralrnmpo
Expand Down Expand Up @@ -136825,7 +136825,7 @@ F C_ ( CC X. X ) ) $=
A e. X ) ) -> ( R " { A } ) e. K ) $=
( vy ctop wcel wa cima cuni wss adantr eqid syl2anc wceq ad2antll ctopon
co ctx csn cv cop cmpt ccnv crab nfv nfcv nfrab1 cxp txtop simprl eltopss
txuni sseqtr4d imass1 syl xpimasn sseqtrd sseld pm4.71rd wb elimasng elvd
txuni sseqtrrd imass1 syl xpimasn sseqtrd sseld pm4.71rd wb elimasng elvd
cvv anbi2d bitrd rabid syl6bbr eqrd mptpreima syl6eqr ccn toptopon biimpi
cfv ad2antlr ad2antrr simprr cnmptc cnmptid cnmpt1t cnima eqeltrd ) CHIZD
HIZJZBCDUATZIZAEIZJZJZBAUBZKZGDLZAGUCZUDZUEZUFBKZDWMWOWRBIZGWPUGZWTWMGWOX
Expand Down Expand Up @@ -136962,7 +136962,7 @@ F C_ ( CC X. X ) ) $=
( wcel wss cima cnt cfv ccnv ccn adantr wceq cnntri syl2anc syl imacnvcnv
co chmeo wa cuni hmeocn crn imassrn wf1o wfo eqid hmeof1o f1ofo forn 3syl
sseqtrid wf1 f1of1 f1imacnv sylancom fveq2d sseqtrd wfun wi f1ofun cntop2
ctop ntrss3 sseqtr4d funimass1 mpd hmeocnvcn sylan fveq2i 3sstr3g eqssd )
ctop ntrss3 sseqtrrd funimass1 mpd hmeocnvcn sylan fveq2i 3sstr3g eqssd )
BCDUATGZAEHZUBZBAIZDJKZKZBACJKZKZIZVQBLZVTIZWBHZVTWCHZVQWEWDVRIZWAKZWBVQB
CDMTGZVRDUCZHZWEWIHVOWJVPBCDUDNZVQBUEZVRWKBAUFVQEWKBUGZEWKBUHWNWKOVOWOVPB
CDEWKFWKUIZUJNZEWKBUKEWKBULUMZUNZVRBCDWKWPPQVQWHAWAVOVPEWKBUOZWHAOVQWOWTW
Expand Down Expand Up @@ -138526,7 +138526,7 @@ the base set to the (extended) reals and which is nonnegative, symmetric
blssec $p |- ( ( D e. ( *Met ` X ) /\ P e. X /\ S e. RR* ) ->
( P ( ball ` D ) S ) C_ [ P ] .~ ) $=
( cxmet cfv wcel cxr w3a cbl co cpnf cec wss wa cle wbr pnfge adantl ssbl
wi pnfxr 3expia mpanr2 mpd 3impa wceq xmetec 3adant3 sseqtr4d ) AEGHIZBEI
wi pnfxr 3expia mpanr2 mpd 3impa wceq xmetec 3adant3 sseqtrrd ) AEGHIZBEI
ZDJIZKBDALHZMZBNUPMZBCOZUMUNUOUQURPZUMUNQZUOQDNRSZUTUOVBVADTUAVAUONJIZVBU
TUCUDVAUOVCQVBUTABDNEUBUEUFUGUHUMUNUSURUIUOABCEFUJUKUL $.
$}
Expand Down Expand Up @@ -138986,7 +138986,7 @@ the base set to the (extended) reals and which is nonnegative, symmetric
$( The balls of a metric space are open sets. (Contributed by NM,
12-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) $)
blssopn $p |- ( D e. ( *Met ` X ) -> ran ( ball ` D ) C_ J ) $=
( cxmet cfv wcel cbl crn ctg ctb wss blbas bastg syl mopnval sseqtr4d ) A
( cxmet cfv wcel cbl crn ctg ctb wss blbas bastg syl mopnval sseqtrrd ) A
CEFGZAHFIZSJFZBRSKGSTLACMSKNOABCDPQ $.

$( The union of a collection of open sets of a metric space is open.
Expand Down Expand Up @@ -139535,7 +139535,7 @@ S C_ ( P ( ball ` D ) T ) ) $=
crn ctg cfv cbl wceq wrex wb eqid elrnmpog biimpi adantl xpeq1 eqeq2d
cvv elv xpeq2 cbvrex2v sylib simplll simplrl simplrr cuni wral ctopon
simpr cxmet mopntopon syl adantr simprl toponss syl2anc simprr xpss12
xmetxp unirnbl sseqtr4d c1st ad2antrr xp1st mopni2 syl3anc c2nd xp2nd
xmetxp unirnbl sseqtrrd c1st ad2antrr xp1st mopni2 syl3anc c2nd xp2nd
crp cpr cxr clt cinf wfn cpw wf blf ffnd ad4antr sselda rpxr ad2antrl
xrmincl fnovrn eleq2 anbi12d xrminrpcl blcntr xmetxpbl cle wbr sseldd
sseq1 xrmin1inf ssbl syl221anc sstrd xrmin2inf jca rspcedvd rexlimddv
Expand Down Expand Up @@ -139635,7 +139635,7 @@ S C_ ( P ( ball ` D ) T ) ) $=
A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) ) ) ) $=
( cfv wcel co crp wral wa wi cxmet w3a ccnp cbl cima wss wrex clt metcnp3
wf cv wbr wb wfun cdm ffun ad2antlr simpll1 simpll3 rpxr ad2antll syl3anc
cxr blssm wceq fdm sseqtr4d funimass4 syl2anc elbl imbi1d impexp ad2antrr
cxr blssm wceq fdm sseqtrrd funimass4 syl2anc elbl imbi1d impexp ad2antrr
simpl2 simplrl rpxrd simpllr adantr ffvelrnd simplr elbl2 syl22anc imbi2d
ffvelrnda pm5.74da syl5bb ralbidv2 anassrs rexbidva ralbidva pm5.32da
bitrd ) DJUANOZEKUANOZFJOZUBZGFHIUCPNOJKGUJZGFBUKZDUDNPZUEFGNZAUKZEUDNPZU
Expand Down Expand Up @@ -147835,7 +147835,7 @@ a singleton (where the latter can also be thought of as representing
( vj vk vf xnninf com cv wceq c1o cfv wcel c2o wss adantr adantl fveq2d
c0 cuni cif cmpt cmap co csuc wral wf wa a1i nninff nnpredcl ffvelrnd wdc
1lt2o nndceq0 ifcldcd eqid fmptd cvv wb 2onn omex elmapg mp2an sylibr wtr
wn 1on ontrci peano2 syl df-2o syl6eleq trsucss mpsyl sseqtr4d word simpr
wn 1on ontrci peano2 syl df-2o syl6eleq trsucss mpsyl sseqtrrd word simpr
iftrue nnord ordtr unisucg mpbid wne neqned nnsucpred syl2anc suceq fveq2
3syl sseq12d fveq1 ralbidv df-nninf elrab2 simprbi cbvralv sylib ad2antrr
rspcdva eqsstrrd eqsstrd peano3 neneqd ad2antlr iffalsed 3sstr4d mpjaodan
Expand Down Expand Up @@ -148070,7 +148070,7 @@ C_ if ( A. k e. suc J ( Q ` ( i e. _om
|-> if ( i e. k , 1o , (/) ) ) ) = 1o
, 1o , (/) ) ) $=
( c2o xnninf cmap co wcel com wa c1o c0 cif wceq csuc wral wss syl adantl
wel cfv peano2 nninfsellemcl el2oss1o sylan2 adantr iftrue sseqtr4d simpl
wel cfv peano2 nninfsellemcl el2oss1o sylan2 adantr iftrue sseqtrrd simpl
wn csn con3i cun df-suc raleqi ralunb bitri sylnibr iffalsed 0ss syl6eqss
cmpt wdc wo nninfsellemdc exmiddc mpjaodan ) AEFGHIZDJIZKZBJBCUALMNVCAUBL
OZCDPZQZVLCVMPZQZLMNZVNLMNZRZVNUKZVKVNKVQLVRVKVQLRZVNVJVIVMJIZWADUCVIWBKV
Expand Down
Loading