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..ffa68c561 100644 --- a/set.mm +++ b/set.mm @@ -33834,6 +33834,13 @@ 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 $. + + $( 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 + ST $. $} ${ @@ -41684,6 +41691,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.) $) @@ -99316,6 +99328,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 @@ -473556,11 +473574,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 ) ) $= @@ -513604,17 +513617,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 +513907,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 +515468,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 $. $} ${ @@ -532429,15 +532431,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 $. @@ -532452,17 +532445,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 ) ) $= @@ -555369,15 +555351,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 +581106,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,24 +581487,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 $. - $( 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.) $) - 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.) $) @@ -582200,38 +582162,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 ceqsralbv + wi breq2 bitr3i idinxpss ralin 3bitr4i ) AFZEFZGZUEUFDHZSZECIZABIUECJUEUE + DHZSZABIKBCLMDNUKABCMIUJULABUJUFUEGZUHSZECIULUNUIECUMUGUHEAOPQUHUKEUECUFU + EUEDTRUAQAEBCDUBUKABCUCUD $. $} ${ @@ -587076,8 +587016,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 +587047,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 +587324,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 +587336,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 +587384,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 +587509,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 +587582,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