From 70c3cfc5beb9d2aa78e7dc16592d7bd2c30a6901 Mon Sep 17 00:00:00 2001 From: Benoit <41090811+benjub@users.noreply.github.com> Date: Fri, 29 Dec 2023 17:57:32 +0100 Subject: [PATCH] Add dmep, rnep (#3723) --- changes-set.txt | 7 ++-- discouraged | 2 ++ set.mm | 93 ++++++++++++++++++++++++++++++------------------- 3 files changed, 65 insertions(+), 37 deletions(-) diff --git a/changes-set.txt b/changes-set.txt index 563ea35cfc..2f89850296 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -83,6 +83,9 @@ make a github issue.) DONE: Date Old New Notes +28-Dec-23 eqri [same] moved from TA's mathbox to main set.mm +28-Dec-23 domep dmep moved from SF's mathbox to main set.mm +28-Dec-23 compel velcomp moved from AS's mathbox to main set.mm 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 @@ -1181,8 +1184,8 @@ Date Old New Notes 18-Jul-20 0fallfac [same] moved from SF's mathbox to main set.mm 18-Jul-20 fallfacfwd [same] moved from SF's mathbox to main set.mm 18-Jul-20 risefacfac [same] moved from SF's mathbox to main set.mm -18-Jul-20 fallfac1 [same] moved from SF's mathbox to main set.mm -18-Jul-20 risefac1 [same] moved from SF's mathbox to main set.mm +18-Jul-20 fallfac1 [same] moved from SF's mathbox to main set.mm +18-Jul-20 risefac1 [same] moved from SF's mathbox to main set.mm 18-Jul-20 fallfacp1d [same] moved from SF's mathbox to main set.mm 18-Jul-20 risefacp1d [same] moved from SF's mathbox to main set.mm 18-Jul-20 fallfacp1 [same] moved from SF's mathbox to main set.mm diff --git a/discouraged b/discouraged index 383d6d1554..9d3b21fccd 100755 --- a/discouraged +++ b/discouraged @@ -14837,6 +14837,7 @@ New usage of "dochord2N" is discouraged (0 uses). New usage of "dochpolN" is discouraged (0 uses). New usage of "dochsordN" is discouraged (0 uses). New usage of "dochspocN" is discouraged (0 uses). +New usage of "domepOLD" is discouraged (0 uses). New usage of "dral1-o" is discouraged (4 uses). New usage of "dral1ALT" is discouraged (0 uses). New usage of "dral2-o" is discouraged (4 uses). @@ -18323,6 +18324,7 @@ Proof modification of "dju1p1e2" is discouraged (72 steps). Proof modification of "dju1p1e2ALT" is discouraged (34 steps). Proof modification of "djuexALT" is discouraged (51 steps). Proof modification of "dmtrclfvRP" is discouraged (46 steps). +Proof modification of "domepOLD" is discouraged (51 steps). Proof modification of "dral1ALT" is discouraged (34 steps). Proof modification of "dral2-o" is discouraged (14 steps). Proof modification of "drnfc1OLD" is discouraged (52 steps). diff --git a/set.mm b/set.mm index b984701a86..e907e84543 100644 --- a/set.mm +++ b/set.mm @@ -36149,6 +36149,11 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use ( wcel cdif wne wn wa eldif nelne2 ex adantld syl5bi imp ) CAEZDBAFEZCDGZQD BEZDAEHZIPRDBAJPTRSPTRCDAKLMNO $. + $( Characterization of setvar elements of the complement of a class. + (Contributed by Andrew Salmon, 15-Jul-2011.) $) + velcomp $p |- ( x e. ( _V \ A ) <-> -. x e. A ) $= + ( cv cvv cdif wcel wn vex eldif mpbiran ) ACZDBEFKDFKBFGAHKDBIJ $. + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -36455,6 +36460,17 @@ technically classes despite morally (and provably) being sets, like ` 1 ` $. $} + ${ + eqri.1 $e |- F/_ x A $. + eqri.2 $e |- F/_ x B $. + eqri.3 $e |- ( x e. A <-> x e. B ) $. + $( Infer equality of classes from equivalence of membership. (Contributed + by Thierry Arnoux, 7-Oct-2017.) $) + eqri $p |- A = B $= + ( wceq wtru nftru cv wcel wb a1i eqrd mptru ) BCGHABCAIDEAJZBKPCKLHFMNO + $. + $} + ${ $d A x $. $d B x $. $d ph x $. eqelssd.1 $e |- ( ph -> A C_ B ) $. @@ -53164,6 +53180,25 @@ Contrast with domain (defined in ~ df-dm ). For alternate definitions, CDAGHIJ $. $} + ${ + $d x y $. + $( The domain of the membership relation is the universal class. + (Contributed by Scott Fenton, 27-Oct-2010.) (Proof shortened by BJ, + 26-Dec-2023.) $) + dmep $p |- dom _E = _V $= + ( vx vy cep cdm cvv wceq cv wcel eqv wbr wex wel el epel exbii mpbir eldm + vex mpgbir ) CDZEFAGZTHZAATIUBUABGCJZBKZUDABLZBKABMUCUEBBUANOPBUACARQPS + $. + + $( Obsolete proof of ~ dmep as of 26-Dec-2023. (Contributed by Scott + Fenton, 27-Oct-2010.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + domepOLD $p |- dom _E = _V $= + ( vx vy weq cab cv cep wbr wex cvv cdm equid wel el exbii mpbir 2th abbii + epel df-v df-dm 3eqtr4ri ) AACZADAEZBEFGZBHZADIFJUBUEAUBUEAKUEABLZBHABMUD + UFBBUCRNOPQASABFTUA $. + $} + ${ $d x y A $. $( An empty domain is equivalent to an empty range. (Contributed by NM, @@ -53174,7 +53209,26 @@ Contrast with domain (defined in ~ df-dm ). For alternate definitions, ZCFZBGZHIZUKBFZCGZHIZAUAZHIAUBZHIULUIHJZKZBLZUOUJHJZKZCLZUNUQULRZBLZUORZC LZVBVEVGUOCFZRVIVGULBFVJULBMUKBCUCUDUOCMUEVFVABUTULUINSOVHVDCVCUOUJNSOUFU LBHPUOCHPQURUMHBCAUGTUSUPHBCAUHTQ $. + $} + + $( The range of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] + p. 36. (Contributed by NM, 4-Jul-1994.) $) + rn0 $p |- ran (/) = (/) $= + ( c0 cdm wceq crn dm0 dm0rn0 mpbi ) ABACADACEAFG $. + + ${ + $d x y $. + $( The range of the membership relation is the universal class minus the + empty set. (Contributed by BJ, 26-Dec-2023.) $) + rnep $p |- ran _E = ( _V \ { (/) } ) $= + ( vy vx cep crn cv wbr wex cab cvv c0 csn cdif dfrn2 nfab1 nfcv wcel abid + wn bicomi 3bitri wel wceq epel exbii neq0 velsn notbii velcomp eqri eqtri + ) CDAEZBEZCFZAGZBHZIJKZLZABCMBUOUQUNBNBUQOULUOPUNULUPPZRZULUQPZUNBQUNABUA + ZAGZULJUBZRZUSUMVAABUKUCUDVDVBAULUESVCURURVCBJUFSUGTUTUSBUPUHSTUIUJ $. + $} + ${ + $d x y A $. $( A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.) $) reldm0 $p |- ( Rel A -> ( A = (/) <-> dom A = (/) ) ) $= @@ -53439,11 +53493,6 @@ Contrast with domain (defined in ~ df-dm ). For alternate definitions, NRABGOABCDEHFPQ $. $} - $( The range of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] - p. 36. (Contributed by NM, 4-Jul-1994.) $) - rn0 $p |- ran (/) = (/) $= - ( c0 cdm wceq crn dm0 dm0rn0 mpbi ) ABACADACEAFG $. - ${ $d y A $. $d y B $. $d x y $. $( Alternate definition of indexed union when ` B ` is a set. (Contributed @@ -457052,17 +457101,6 @@ and the expression ( x e. A /\ x e. B ) ` . JKLMNOPUOUPUQ $. $} - ${ - eqri.1 $e |- F/_ x A $. - eqri.2 $e |- F/_ x B $. - eqri.3 $e |- ( x e. A <-> x e. B ) $. - $( Infer equality of classes from equivalence of membership. (Contributed - by Thierry Arnoux, 7-Oct-2017.) $) - eqri $p |- A = B $= - ( wceq wtru nftru cv wcel wb a1i eqrd mptru ) BCGHABCAIDEAJZBKPCKLHFMNO - $. - $} - ${ $d A x $. $d B x $. $( A definition of ` -. A e. B ` . (Contributed by Thierry Arnoux, @@ -513695,16 +513733,6 @@ Set induction (or epsilon induction) YGWCXJWDCYNWCWEWFWHWIWJWPWKWLWMWNWO $. $} - ${ - $d x y $. - $( The domain of the membership relation is the universe. (Contributed by - Scott Fenton, 27-Oct-2010.) $) - domep $p |- dom _E = _V $= - ( vx vy weq cab cv cep wbr wex cvv cdm equid wel el exbii mpbir 2th abbii - epel df-v df-dm 3eqtr4ri ) AACZADAEZBEFGZBHZADIFJUBUEAUBUEAKUEABLZBHABMUD - UFBBUCRNOPQASABFTUA $. - $} - ${ $d F g $. $d I g $. $( The value of the recursive definition generator at ` (/) ` when the base @@ -654491,17 +654519,12 @@ notation for set theory (it is not defined in the predicate calculus IUEUCAUDJAUDUBKZUHCZUFUGAUDUBUBELUCAUDEMUIUHUHFZGUEUGUHUHNUEUJUFUEUHUDUHUDA UDEOZUKPQRSTUDENUA $. - $( Equivalence between two ways of saying "is a member of the complement of - ` A ` ". (Contributed by Andrew Salmon, 15-Jul-2011.) $) - compel $p |- ( x e. ( _V \ A ) <-> -. x e. A ) $= - ( cv cvv cdif wcel wn vex eldif mpbiran ) ACZDBEFKDFKBFGAHKDBIJ $. - ${ $d x A $. $( Equality between two ways of saying "the complement of ` A ` ". (Contributed by Andrew Salmon, 15-Jul-2011.) $) compeq $p |- ( _V \ A ) = { x | -. x e. A } $= - ( cv wcel wn cvv cdif compel abbi2i ) ACBDEAFBGABHI $. + ( cv wcel wn cvv cdif velcomp abbi2i ) ACBDEAFBGABHI $. $} $( The complement of ` A ` is not equal to ` A ` . (Contributed by Andrew @@ -654515,9 +654538,9 @@ notation for set theory (it is not defined in the predicate calculus by Andrew Salmon, 15-Jul-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) $) compab $p |- ( _V \ { z | ph } ) = { z | -. ph } $= - ( cvv cab cdif wn wceq cv wcel wb nfcv nfab1 nfdif cleqf abid notbii compel - 3bitr4i mpgbir ) CABDZEZAFZBDZGBHZUAIZUDUCIZJBBUAUCBCTBCKABLMUBBLNUDTIZFUBU - EUFUGAABOPBTQUBBORS $. + ( cvv cdif wn wceq cv wcel wb nfcv nfab1 nfdif cleqf notbii velcomp 3bitr4i + cab abid mpgbir ) CABQZDZAEZBQZFBGZUAHZUDUCHZIBBUAUCBCTBCJABKLUBBKMUDTHZEUB + UEUFUGAABRNBTOUBBRPS $. $( Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.) $)