Merge branch 'develop' into av-alg1

avekens · Dec 30, 2023 · 1d6e6ea · 1d6e6ea
2 parents 626b412 + 70c3cfc
commit 1d6e6ea
Show file tree

Hide file tree

Showing 3 changed files with 65 additions and 37 deletions.
diff --git a/changes-set.txt b/changes-set.txt
@@ -84,6 +84,9 @@ make a github issue.)
 DONE:
 Date      Old       New         Notes
 29-Dec-23 uzidd     [same]      moved from GS's mathbox to main set.mm
+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
@@ -1182,8 +1185,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
@@ -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
@@ -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
@@ -457062,17 +457111,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,
@@ -513705,16 +513743,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
@@ -654501,17 +654529,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
@@ -654525,9 +654548,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.) $)