From 4493138ea5ae47449974ffd29b2a4c98731823d1 Mon Sep 17 00:00:00 2001 From: mazsa Date: Sun, 12 Jan 2025 13:10:13 +0100 Subject: [PATCH 1/5] disjcsn/bnj521 to main --- discouraged | 3 -- set.mm | 87 +++++++++++++++++++++-------------------------------- 2 files changed, 34 insertions(+), 56 deletions(-) diff --git a/discouraged b/discouraged index 827ff48e8..abf0cc823 100644 --- a/discouraged +++ b/discouraged @@ -2441,8 +2441,6 @@ "bnj518" is used by "bnj546". "bnj519" is used by "bnj535". "bnj519" is used by "bnj97". -"bnj521" is used by "bnj535". -"bnj521" is used by "bnj927". "bnj523" is used by "bnj600". "bnj523" is used by "bnj908". "bnj523" is used by "bnj934". @@ -15157,7 +15155,6 @@ New usage of "bnj446" is discouraged (3 uses). New usage of "bnj517" is discouraged (1 uses). New usage of "bnj518" is discouraged (2 uses). New usage of "bnj519" is discouraged (2 uses). -New usage of "bnj521" is discouraged (2 uses). New usage of "bnj523" is discouraged (3 uses). New usage of "bnj524" is discouraged (0 uses). New usage of "bnj525" is discouraged (7 uses). diff --git a/set.mm b/set.mm index 1e662247a..7ed29919c 100644 --- a/set.mm +++ b/set.mm @@ -99316,6 +99316,12 @@ is that it denies the existence of a set containing itself ( ~ elirrv ). ( cv wnel cab cvv vprc nelir wceq wb ruv neleq1 ax-mp mpbir ) ABZNCADZECZEE CZEEFGOEHPQIAJOEEKLM $. + $( A class is disjoint from its singleton. A consequence of regularity. + (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by BJ, + 4-Apr-2019.) $) + disjcsn $p |- ( A i^i { A } ) = (/) $= + ( csn cin c0 wceq wcel wn elirr disjsn mpbir ) AABCDEAAFGAHAAIJ $. + ${ $d x y A $. $( The membership relation is well-founded on any class. (Contributed by @@ -513604,17 +513610,6 @@ conditions of the Five Segment Axiom ( ~ axtg5seg ). See ~ df-ofs . ( cvv wcel cop csn wfun funsng mpan ) ADEBDEABFGHCABDDIJ $. $} - ${ - $d A x $. - $( First-order logic and set theory. (Contributed by Jonathan Ben-Naim, - 3-Jun-2011.) (New usage is discouraged.) $) - bnj521 $p |- ( A i^i { A } ) = (/) $= - ( vx csn cin c0 wne wn wceq cv wcel wex elirr wa elin velsn eleq1 biimpac - sylan2b sylbi exlimiv mto n0 mtbir nne mpbi ) AACZDZEFZGUGEHUHBIZUGJZBKZU - KAAJZALUJULBUJUIAJZUIUFJZMULUIAUFNUNUMUIAHZULBAOUOUMULUIAAPQRSTUABUGUBUCU - GEUDUE $. - $} - ${ bnj524.1 $e |- ( ph <-> ps ) $. bnj524.2 $e |- A e. _V $. @@ -513905,10 +513900,10 @@ conditions of the Five Segment Axiom ( ~ axtg5seg ). See ~ df-ofs . $( First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) $) bnj927 $p |- ( ( p = suc n /\ f Fn n ) -> G Fn p ) $= - ( cv csuc wceq wfn wa csn cun cop simpr vex fnsn a1i cin c0 bnj521 fneq1i - fnund sylibr df-suc eqeq2i biimpi adantr fneq2d mpbird ) EHZCHZIZJZBHZUMK - ZLZDULKDUMUMMZNZKZURUPUMAOMZNZUTKVAURUMUSUPVBUOUQPVBUSKURUMACQGRSUMUSTUAJ - URUMUBSUDUTDVCFUCUEURULUTDUOULUTJZUQUOVDUNUTULUMUFUGUHUIUJUK $. + ( cv csuc wceq wfn wa csn cun cop simpr vex fnsn a1i cin c0 disjcsn fnund + fneq1i sylibr df-suc eqeq2i biimpi adantr fneq2d mpbird ) EHZCHZIZJZBHZUM + KZLZDULKDUMUMMZNZKZURUPUMAOMZNZUTKVAURUMUSUPVBUOUQPVBUSKURUMACQGRSUMUSTUA + JURUMUBSUCUTDVCFUDUEURULUTDUOULUTJZUQUOVDUNUTULUMUFUGUHUIUJUK $. $} ${ @@ -515466,12 +515461,12 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a n ) $= ( cv wfn cvv w-bnj15 csn cun wceq w-bnj17 bnj422 bnj251 bitri cfv c-bnj14 ciun cop wcel wfun wral fvex bnj518 iunexg sylancr vex bnj519 syl dmsnopg - wa cdm bnj1422 cin c0 bnj521 mpan2 sylan2 fneq1i sylibr fneq2 syl5ibr imp - fnun sylbi ) DEUAZAIRZHRZWAUBZUCZUDZFRZWASZUEZWDWFVSAVDZVDZVDZJVTSZWGWDWF - VSAUEWJVSAWDWFUFWDWFVSAUGUHWDWIWKWIWKWDJWCSZWIWEWACKRZWEUIZDECRUJZUKZULUB - ZUCZWCSZWLWHWFWQWBSZWSWHWQWBWHWPTUMZWQUNWHWNTUMWOTUMCWNUOXAWMWEUPLMABCDEF - GHKNOQUQCWNWOTTURUSZWAWPHUTVAVBWHXAWQVEWBUDXBWAWPTVCVBVFWFWTVDWAWBVGVHUDW - SWAVIWAWBWEWQVQVJVKWCJWRPVLVMVTWCJVNVOVPVR $. + wa cdm bnj1422 cin c0 disjcsn fnun mpan2 sylan2 fneq1i sylibr syl5ibr imp + fneq2 sylbi ) DEUAZAIRZHRZWAUBZUCZUDZFRZWASZUEZWDWFVSAVDZVDZVDZJVTSZWGWDW + FVSAUEWJVSAWDWFUFWDWFVSAUGUHWDWIWKWIWKWDJWCSZWIWEWACKRZWEUIZDECRUJZUKZULU + BZUCZWCSZWLWHWFWQWBSZWSWHWQWBWHWPTUMZWQUNWHWNTUMWOTUMCWNUOXAWMWEUPLMABCDE + FGHKNOQUQCWNWOTTURUSZWAWPHUTVAVBWHXAWQVEWBUDXBWAWPTVCVBVFWFWTVDWAWBVGVHUD + WSWAVIWAWBWEWQVJVKVLWCJWRPVMVNVTWCJVQVOVPVR $. $} ${ @@ -555369,15 +555364,9 @@ FOL part ( ~ bj-ru0 ) and then two versions ( ~ bj-ru1 and ~ bj-ru ). ( c0 wne cv wcel wex n0 mpbi ) BDEAFBGAHCABIJ $. $} - $( A class is disjoint from its singleton. A consequence of regularity. - Shorter proof than ~ bnj521 and does not depend on ~ df-ne . (Contributed - by BJ, 4-Apr-2019.) $) - bj-disjcsn $p |- ( A i^i { A } ) = (/) $= - ( csn cin c0 wceq wcel wn elirr disjsn mpbir ) AABCDEAAFGAHAAIJ $. - $( Disjointness of the singletons containing 0 and 1. This is a consequence - of ~ bj-disjcsn but the present proof does not use regularity. - (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.) $) + of ~ disjcsn but the present proof does not use regularity. (Contributed + by BJ, 4-Apr-2019.) (Proof modification is discouraged.) $) bj-disjsn01 $p |- ( { (/) } i^i { 1o } ) = (/) $= ( c0 c1o wne csn cin wceq 1n0 necomi disjsn2 ax-mp ) ABCADBDEAFBAGHABIJ $. @@ -581130,7 +581119,7 @@ A collection of theorems for commuting equalities (or #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# $) - $( Contents: ~ https://us.metamath.org/mpeuni/mmtheorems.html#dtl:20.21 $) + $( Contents: ~ https://us.metamath.org/mpeuni/mmtheorems.html#dtl:20.22 $) $( @@ -581511,13 +581500,6 @@ A collection of theorems for commuting equalities (or suceqsneq $p |- ( A e. V -> ( suc A = suc B <-> { A } = { B } ) ) $= ( wcel csuc wceq csn suc11reg sneqbg bitr4id ) ACDAEBEFABFAGBGFABHABCIJ $. - $( A class is disjoint from its singleton. A consequence of regularity. - Shorter proof than ~ bnj521 and does not depend on ~ df-ne . (Temporary: - as soon as this Mathbox only PR is accepted, I'll open a PR to place this - to the main. PM) (Contributed by BJ, 4-Apr-2019.) $) - disjcsn $p |- ( A i^i { A } ) = (/) $= - ( csn cin c0 wceq wcel wn elirr disjsn mpbir ) AABCDEAAFGAHAAIJ $. - $( An equality involving class union and class difference. (Temporary: as soon as this Mathbox only PR is accepted, I'll open a PR to place this to the main. PM) (Contributed by Thierry Arnoux, 26-Jun-2024.) $) @@ -587076,8 +587058,8 @@ the null class is disjoint (which it is, see ~ disjALTV0 ). (Contributed eqvrel1cossinidres $p |- EqvRel ,~ ( R i^i ( _I |` A ) ) $= ( cid cres cin disjALTVinidres disjimi ) BCADEABFG $. - $( The cosets by a tail Cartesian product with a restricted identity relation - are in equivalence relation. (Contributed by Peter Mazsa, + $( The cosets by a range Cartesian product with a restricted identity + relation are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.) $) eqvrel1cossxrnidres $p |- EqvRel ,~ ( R |X. ( _I |` A ) ) $= ( cid cres cxrn disjALTVxrnidres disjimi ) BCADEABFG $. @@ -587107,8 +587089,8 @@ the null class is disjoint (which it is, see ~ disjALTV0 ). (Contributed EqvRel ,~ ( R i^i ( _I |` A ) ) ) $= ( cid cres cin disjALTVinidres detlem ) BCADEABFG $. - $( The cosets by the tail Cartesian product with the restricted identity - relation are in equivalence relation if and only if the tail Cartesian + $( The cosets by the range Cartesian product with the restricted identity + relation are in equivalence relation if and only if the range Cartesian product with the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.) $) detxrnidres $p |- ( Disj ( R |X. ( _I |` A ) ) <-> @@ -587384,8 +587366,8 @@ implies disjointness (e.g. ~ eqvrelqseqdisj5 ), or converse function wceq dfpart2 dferALTV2 3bitr4i ) BCADEZFSGSHAOISJZKTGTHAOIASLATMABNASPATQR $. - $( Class ` A ` is a partition by a tail Cartesian product with the identity - class restricted to it if and only if the cosets by the tail Cartesian + $( Class ` A ` is a partition by a range Cartesian product with the identity + class restricted to it if and only if the cosets by the range Cartesian product are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.) $) petxrnidres2 $p |- ( ( Disj ( R |X. ( _I |` A ) ) /\ @@ -587396,9 +587378,9 @@ implies disjointness (e.g. ~ eqvrelqseqdisj5 ), or converse function ,~ ( R |X. ( _I |` A ) ) ) = A ) ) $= ( cid cres cxrn disjALTVxrnidres petlemi ) ABCADEABFG $. - $( A class is a partition by a tail Cartesian product with the identity class - restricted to it if and only if the cosets by the tail Cartesian product - are in equivalence relation on it. Cf. ~ br1cossxrnidres , + $( A class is a partition by a range Cartesian product with the identity + class restricted to it if and only if the cosets by the range Cartesian + product are in equivalence relation on it. Cf. ~ br1cossxrnidres , ~ disjALTVxrnidres and ~ eqvrel1cossxrnidres . (Contributed by Peter Mazsa, 31-Dec-2021.) $) petxrnidres $p |- ( ( R |X. ( _I |` A ) ) Part A <-> @@ -587444,7 +587426,7 @@ implies disjointness (e.g. ~ eqvrelqseqdisj5 ), or converse function ( weqvrel cep ccnv cqs cres wdisjALTV cin eqvreldisj3 disjimin syl ) BDEFAB GHZICNJIABKCNLM $. - $( Tail Cartesian product with converse epsilon relation restricted to the + $( Range Cartesian product with converse epsilon relation restricted to the quotient set of an equivalence relation is disjoint. (Contributed by Peter Mazsa, 30-May-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) $) eqvreldisj5 $p |- ( EqvRel R -> Disj ( S |X. ( `' _E |` ( B /. R ) ) ) ) $= @@ -587569,9 +587551,8 @@ is what we used to think of as the partition equivalence theorem (but cf. $( Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are - literally the same. Cf. ~ pet , the general Partition-Equivalence - Theorem, with general ` R ` . (Contributed by Peter Mazsa, - 31-Dec-2024.) $) + literally the same. Cf. ~ pet , the Partition-Equivalence Theorem, with + general ` R ` . (Contributed by Peter Mazsa, 31-Dec-2024.) $) mpets $p |- MembParts = CoMembErs $= ( va cep ccnv cv cres cparts wbr ccoss cers cmembparts ccomembers wb mpets2 cab cvv elv abbii df-membparts df-comembers 3eqtr4i ) BCADZEZUAFGZANUBHUAIG @@ -587643,10 +587624,10 @@ is what we used to think of as the partition equivalence theorem (but cf. $( Partition-Equivalence Theorem with general ` R ` while preserving the restricted converse epsilon relation of ~ mpet2 (as opposed to - ~ petincnvepres ). A class is a partition by a tail Cartesian product + ~ petincnvepres ). A class is a partition by a range Cartesian product with general ` R ` and the restricted converse element class if and only - if the cosets by the tail Cartesian product are in an equivalence relation - on it. Cf. ~ br1cossxrncnvepres . + if the cosets by the range Cartesian product are in an equivalence + relation on it. Cf. ~ br1cossxrncnvepres . This theorem (together with ~ pets and ~ pet2 ) is the main result of my investigation into set theory. It is no more general than the From 6774571e24e23afab839cc382243f259b38d2982 Mon Sep 17 00:00:00 2001 From: mazsa Date: Sun, 12 Jan 2025 14:11:26 +0100 Subject: [PATCH 2/5] undif5 to main --- set.mm | 19 ++++++------------- 1 file changed, 6 insertions(+), 13 deletions(-) diff --git a/set.mm b/set.mm index 7ed29919c..bd3025843 100644 --- a/set.mm +++ b/set.mm @@ -41684,6 +41684,11 @@ disjoint classes (see ~ disjdif ). Part of proof of Corollary 6K of ( wss cun wceq cdif ssequn1 undif2 eqeq1i bitr4i ) ABCABDZBEABAFDZBEABGLKBA BHIJ $. + $( An equality involving class union and class difference. (Contributed by + Thierry Arnoux, 26-Jun-2024.) $) + undif5 $p |- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A ) $= + ( cin c0 wceq cun cdif difun2 disjdif2 eqtrid ) ABCDEABFBGABGAABHABIJ $. + $( A subset of a difference does not intersect the subtrahend. (Contributed by Jeff Hankins, 1-Sep-2013.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) $) @@ -473562,11 +473567,6 @@ Class abstractions (a.k.a. class builders) ( wceq wss wa cdif c0 eqss ssdif0 anbi12i sylbbr ) ABCABDZBADZEABFGCZBAFGCZ EABHLNMOABIBAIJK $. - $( An equality involving class union and class difference. (Contributed by - Thierry Arnoux, 26-Jun-2024.) $) - undif5 $p |- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A ) $= - ( cin c0 wceq cun cdif difun2 disjdif2 eqtrid ) ABCDEABFBGABGAABHABIJ $. - $( Two ways to express equality relative to a class ` A ` . (Contributed by Thierry Arnoux, 23-Jun-2024.) $) indifbi $p |- ( ( A i^i B ) = ( A i^i C ) <-> ( A \ B ) = ( A \ C ) ) $= @@ -581500,17 +581500,10 @@ A collection of theorems for commuting equalities (or suceqsneq $p |- ( A e. V -> ( suc A = suc B <-> { A } = { B } ) ) $= ( wcel csuc wceq csn suc11reg sneqbg bitr4id ) ACDAEBEFABFAGBGFABHABCIJ $. - $( An equality involving class union and class difference. (Temporary: as - soon as this Mathbox only PR is accepted, I'll open a PR to place this to - the main. PM) (Contributed by Thierry Arnoux, 26-Jun-2024.) $) - undif5TEMP $p |- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A ) $= - ( cin c0 wceq cun cdif difun2 disjdif2 eqtrid ) ABCDEABFBGABGAABHABIJ $. - $( Absorption of union with a singleton by difference. (Contributed by Peter Mazsa, 24-Jul-2024.) $) sucdifsn2 $p |- ( ( A u. { A } ) \ { A } ) = A $= - ( csn cin c0 wceq cun cdif disjcsn undif5TEMP ax-mp ) AABZCDEAKFKGAEAHAKIJ - $. + ( csn cin c0 wceq cun cdif disjcsn undif5 ax-mp ) AABZCDEAKFKGAEAHAKIJ $. $( The difference between the successor and the singleton of a class is the class. (Contributed by Peter Mazsa, 20-Sep-2024.) $) From f2d0fc0f3546573c8eda861a25a7765a1f7fe93a Mon Sep 17 00:00:00 2001 From: mazsa Date: Sun, 12 Jan 2025 18:11:28 +0100 Subject: [PATCH 3/5] ceqsrexv2 ceqsralv2 to main --- set.mm | 62 +++++++++++++++------------------------------------------- 1 file changed, 16 insertions(+), 46 deletions(-) diff --git a/set.mm b/set.mm index bd3025843..e938d7c45 100644 --- a/set.mm +++ b/set.mm @@ -33834,6 +33834,18 @@ general is seen either by substitution (when the variable ` V ` has no ( wcel cv wceq wa wrex r19.42v eleq1 adantr pm5.32ri bicomi baib ceqsrexv wb rexbiia pm5.32i 3bitr3i ) DEGZCHZDIZAJZJZCEKUCUFCEKZJUHUCBJUCUFCELUGUF CEUGUDEGZUFUIUFJUGUFUIUCUEUIUCSAUDDEMNOPQTUCUHBABCDEFRUAUB $. + + $( Alternate elimitation of a restricted existential quantifier, using + implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.) $) + ceqsrexv2 $p |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) ) $= + ( ceqsrexbv ) ABCDEFG $. + + $( Alternate elimination of a restricted universal quantifier, using + implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.) $) + ceqsralv2 $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $= + ( cv wceq wi wral wcel wn wa wrex notbid ceqsrexv2 rexanali annim 3bitr3i + con4bii ) CGDHZAICEJZDEKZBIZUAALZMCENUCBLZMUBLUDLUEUFCDEUAABFOPUAACEQUCBR + ST $. $} ${ @@ -532424,15 +532436,6 @@ Real and complex numbers (cont.) brtpid3 $p |- A { C , D , <. A , B >. } B $= ( cop ctp wbr wcel opex tpid3 df-br mpbir ) ABCDABEZFZGMNHCDMABIJABNKL $. - ${ - $d A x $. $d B x $. $d ps x $. - ceqsrexv2.1 $e |- ( x = A -> ( ph <-> ps ) ) $. - $( Alternate elimitation of a restricted existential quantifier, using - implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.) $) - ceqsrexv2 $p |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) ) $= - ( ceqsrexbv ) ABCDEFG $. - $} - ${ $d x V $. $d A y $. $d ps y $. $d x y $. iota5f.1 $e |- F/ x ph $. @@ -532447,17 +532450,6 @@ Real and complex numbers (cont.) GUEVEUTUNBVCDUMTUBUFVCDUQTUCBCIUGUHUIUJ $. $} - ${ - $d x A $. $d x B $. $d ps x $. - ceqsralv2.1 $e |- ( x = A -> ( ph <-> ps ) ) $. - $( Alternate elimination of a restricted universal quantifier, using - implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.) $) - ceqsralv2 $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $= - ( cv wceq wi wral wcel wn wa wrex notbid ceqsrexv2 rexanali annim 3bitr3i - con4bii ) CGDHZAICEJZDEKZBIZUAALZMCENUCBLZMUBLUDLUEUFCDEUAABFOPUAACEQUCBR - ST $. - $} - $( A class is ordinal iff it is a subclass of ` On ` and transitive. (Contributed by Scott Fenton, 21-Nov-2021.) $) dford5 $p |- ( Ord A <-> ( A C_ On /\ Tr A ) ) $= @@ -582175,38 +582167,16 @@ equivalence of domain elementhood (equivalence is not necessary as HUFUEUHPBUCUDQRSTUBUA $. $} - ${ - $d A x $. $d B x $. $d ps x $. - ceqsrexv2TEMP.1 $e |- ( x = A -> ( ph <-> ps ) ) $. - $( Alternate elimitation of a restricted existential quantifier, using - implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.) $) - ceqsrexv2TEMP $p |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) ) $= - ( ceqsrexbv ) ABCDEFG $. - $} - - ${ - $d x A $. $d x B $. $d ps x $. - ceqsralv2TEMP.1 $e |- ( x = A -> ( ph <-> ps ) ) $. - $( Alternate elimination of a restricted universal quantifier, using - implicit substitution. (Temporary: as soon as this Mathbox only PR is - accepted, I'll open a PR to place this to the main. PM) (Contributed by - Scott Fenton, 7-Dec-2020.) $) - ceqsralv2TEMP $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $= - ( cv wceq wi wral wcel wrex notbid ceqsrexv2TEMP rexanali 3bitr3i con4bii - wn wa annim ) CGDHZAICEJZDEKZBIZUAARZSCELUCBRZSUBRUDRUEUFCDEUAABFMNUAACEO - UCBTPQ $. - $} - ${ $d A x y $. $d B x y $. $d R x y $. $( Two ways to say that an intersection of the identity relation with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 12-Dec-2023.) $) ref5 $p |- ( ( _I i^i ( A X. B ) ) C_ R <-> A. x e. ( A i^i B ) x R x ) $= - ( vy cv wceq wbr wi wral wcel cid cxp cin wss equcom imbi1i ceqsralv2TEMP - ralbii breq2 bitr3i idinxpss ralin 3bitr4i ) AFZEFZGZUEUFDHZIZECJZABJUECK - UEUEDHZIZABJLBCMNDOUKABCNJUJULABUJUFUEGZUHIZECJULUNUIECUMUGUHEAPQSUHUKEUE - CUFUEUEDTRUASAEBCDUBUKABCUCUD $. + ( vy cv wceq wbr wral wcel cid cxp cin wss equcom imbi1i ralbii ceqsralv2 + wi breq2 bitr3i idinxpss ralin 3bitr4i ) AFZEFZGZUEUFDHZSZECIZABIUECJUEUE + DHZSZABIKBCLMDNUKABCMIUJULABUJUFUEGZUHSZECIULUNUIECUMUGUHEAOPQUHUKEUECUFU + EUEDTRUAQAEBCDUBUKABCUCUD $. $} ${ From 8a8e0bef8585a727326b7867289e4fa385fd0682 Mon Sep 17 00:00:00 2001 From: mazsa Date: Sun, 12 Jan 2025 23:21:36 +0100 Subject: [PATCH 4/5] deleted ceqsrexv2; ceqsralv2 -> ceqsralbv --- set.mm | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/set.mm b/set.mm index e938d7c45..0fa352551 100644 --- a/set.mm +++ b/set.mm @@ -33835,15 +33835,10 @@ general is seen either by substitution (when the variable ` V ` has no wb rexbiia pm5.32i 3bitr3i ) DEGZCHZDIZAJZJZCEKUCUFCEKZJUHUCBJUCUFCELUGUF CEUGUDEGZUFUIUFJUGUFUIUCUEUIUCSAUDDEMNOPQTUCUHBABCDEFRUAUB $. - $( Alternate elimitation of a restricted existential quantifier, using - implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.) $) - ceqsrexv2 $p |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) ) $= - ( ceqsrexbv ) ABCDEFG $. - $( Alternate elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.) $) - ceqsralv2 $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $= - ( cv wceq wi wral wcel wn wa wrex notbid ceqsrexv2 rexanali annim 3bitr3i + ceqsralbv $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $= + ( cv wceq wi wral wcel wn wa wrex notbid ceqsrexbv rexanali annim 3bitr3i con4bii ) CGDHZAICEJZDEKZBIZUAALZMCENUCBLZMUBLUDLUEUFCDEUAABFOPUAACEQUCBR ST $. $} @@ -582173,7 +582168,7 @@ equivalence of domain elementhood (equivalence is not necessary as Cartesian product is a subclass. (Contributed by Peter Mazsa, 12-Dec-2023.) $) ref5 $p |- ( ( _I i^i ( A X. B ) ) C_ R <-> A. x e. ( A i^i B ) x R x ) $= - ( vy cv wceq wbr wral wcel cid cxp cin wss equcom imbi1i ralbii ceqsralv2 + ( vy cv wceq wbr wral wcel cid cxp cin wss equcom imbi1i ralbii ceqsralbv wi breq2 bitr3i idinxpss ralin 3bitr4i ) AFZEFZGZUEUFDHZSZECIZABIUECJUEUE DHZSZABIKBCLMDNUKABCMIUJULABUJUFUEGZUHSZECIULUNUIECUMUGUHEAOPQUHUKEUECUFU EUEDTRUAQAEBCDUBUKABCUCUD $. From 566eceeca877debb1f9bddb8df3a998960998bf3 Mon Sep 17 00:00:00 2001 From: mazsa Date: Sun, 12 Jan 2025 23:43:35 +0100 Subject: [PATCH 5/5] Minor Deletet "Alternate" form "Alternate elimination". --- set.mm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/set.mm b/set.mm index 0fa352551..ffa68c561 100644 --- a/set.mm +++ b/set.mm @@ -33835,8 +33835,8 @@ general is seen either by substitution (when the variable ` V ` has no wb rexbiia pm5.32i 3bitr3i ) DEGZCHZDIZAJZJZCEKUCUFCEKZJUHUCBJUCUFCELUGUF CEUGUDEGZUFUIUFJUGUFUIUCUEUIUCSAUDDEMNOPQTUCUHBABCDEFRUAUB $. - $( Alternate elimination of a restricted universal quantifier, using - implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.) $) + $( Elimination of a restricted universal quantifier, using implicit + substitution. (Contributed by Scott Fenton, 7-Dec-2020.) $) ceqsralbv $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $= ( cv wceq wi wral wcel wn wa wrex notbid ceqsrexbv rexanali annim 3bitr3i con4bii ) CGDHZAICEJZDEKZBIZUAALZMCENUCBLZMUBLUDLUEUFCDEUAABFOPUAACEQUCBR