double restricted existential uniqueness

[avekens]

A question to the experts:
Are there any interesting statements about double restricted existential uniqueness? I searched for "E! ? e. ? E! ? e. ?" in set.mm, but I found nothing.
I wonder if a theorem analogous to 2eu5 can be proven, maybe
2reu5 $p |- ( ( E! x e. A E! y e. B ph /\ A. x e. A E* y e. B ph ) <-> ( E. x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B  ( ph -> ( x = z /\ y = w ) ) ) ) $=
Has anybody any experience with such a topic?

[Thierry Arnoux]

Hi,

Is the restricted "at most one" quantifier E* y e. B defined?

I have something that could be useful the in the "proba" branch:

  ${
    $d x y A $. $d x B $.
    $( A condition allowing swap of uniqueness and existential quantifiers. $)
    2reuswap2 $p |- ( A. x e. A E* y ( y e. B /\ ph ) -> ( E! x e. A E. y e. B ph -> E! y e. B E. x e. A ph ) ) $=
      ( cv wcel wa wmo wal wrex wreu wex weu df-reu r19.42v df-rex bitr3i bitri
      wi wral df-ral  moanimv albii  bitr4i 2euswap  exbii eubii  3imtr4g sylbi
      an12 ) CFEGZAHZCIZBDUAZBFDGZUMHZCIZBJZACEKZBDLZABDKZCELZTUOUPUNTZBJUSUNBD
      UBURVDBUPUMCUCUDUEUSUQCMZBNZUQBMZCNZVAVCUQBCUFVAUPUTHZBNVFUTBDOVIVEBVIULU
      PAHZHZCMZVEVIVJCEKVLUPACEPVJCEQRVKUQCULUPAUKUGSUHSVCULVBHZCNVHVBCEOVMVGCV
      MUMBDKVGULABDPUMBDQRUHSUIUJ $.
      $( [7-Apr-2017] $)
  $}

BR,

_
Thierry

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Norman Megill]

On Thursday, June 15, 2017 at 9:02:08 PM UTC-4, Thierry Arnoux wrote:

Hi,

Is the restricted "at most one" quantifier E* y e. B defined?

 It hasn't been defined.  Even the unrestricted E* y ph almost never occurs in the literature (there is only one place where I've ever seen it), and I initially hesitated including it since it was nonstandard, but it ended up being useful (now used by 120 theorems).

Some years ago I considered adding E* y e. A ph, but there were only a couple of theorems that would have made use of it  With the overhead of the necessary auxiliary theorems, we wouldn't have saved anything in terms of set.mm size.  I just checked again, and (excluding 6 utility theorems such as reu5) there are now 16 theorems containing the pattern "E* x ( x e. A /\ ...".  While the set.mm size benefit may still be borderline, perhaps it is time to add E* y e. A ph in anticipation of future uses (and also to have a complete set of restricted versions of our quantifiers).  It should be relatively straightforward to retrofit existing theorems.

Norm

[Mázsa Péter]

On Fri, Jun 16, 2017 at 3:49 AM, Norman Megill <n...@alum.mit.edu> wrote:
> On Thursday, June 15, 2017 at 9:02:08 PM UTC-4, Thierry Arnoux wrote:
>>
>> Hi,
>>
>> Is the restricted "at most one" quantifier E* y e. B defined?
>

> While the set.mm size benefit may still be borderline, perhaps it is
> time to add E* y e. A ph in anticipation of future uses (and also to have a
> complete set of restricted versions of our quantifiers).

That would be great Norman. I have 3 theorems (+ a modification) which
could use this simplification:

$( In restricted case, negation of existential uniqueness is nonexistence
or multiple existence.
(Contributed by Peter Mazsa 25-Apr-2017.) $)
nreu $p |- ( -. E! x e. A ph <->
( -. E. x e. A ph \/ -. E* x ( x e. A /\ ph ) ) ) $=
( wreu wn wrex cv wcel wa wmo wo reu5 notbii ianor bitri ) ABCDZE
ABCFZBGCHAIBJZIZEQEREKPSABCLMQRNO $.

$( Sufficient condition for the equivalence of restricted existential
uniqueness and "there exists at most one ` x ` in ` A ` such that
` ph ` ."
(Contributed by Peter Mazsa 25-Apr-2017.) $)
nreu2 $p |- ( E. x e. A ph ->
( E! x e. A ph <-> E* x ( x e. A /\ ph ) ) ) $=
( wrex wreu cv wcel wa wmo wb reu5 a1i bianabs ) ABCDZABCEZBFCGAH
BIZONPHJNABCKLM $.

${
$d x y $. $d A x $. $d A y $.
$( Partition in terms of the definition of disjointness ~ df-disj .
(Contributed by Peter Mazsa 01-Feb-2017.) $)
dfprt3 $p |- ( Prt A <-> A. y E* x ( x e. A /\ y e. x ) ) $=
( wprt cv wdisj wcel wa wmo wal dfprt2 df-disj bitri ) CDACAEZF
NCGBENGHAIBJACKABCNLM $.
$}

${
$d x y $. $d y A $. $d x B $.

$( A condition allowing swap of uniqueness and existential quantifiers.

(Contributed by NM, 14-Nov-2004. modified by Peter Mazsa 18-Mar-2017.) $)
2reuswapALT $p |- ( A. x e. A E* y ( y e. B /\ ph ) ->

( E! x e. A E. y e. B ph -> E! y e. B E. x e. A ph ) ) $=

( cv wcel wa wmo wal wrex wreu wi wex weu df-reu r19.42v df-rex
bitr3i bitri wral df-ral moanimv albii 2euswap an12 exbii eubii
bitr4i 3imtr4g sylbi ) CFEGZAHZCIZBDUAZBFDGZUMHZCIZBJZACEKZBDLZ
ABDKZCELZMUOUPUNMZBJUSUNBDUBURVDBUPUMCUCUDUIUSUQCNZBOZUQBNZCOZV
AVCUQBCUEVAUPUTHZBOVFUTBDPVIVEBVIULUPAHZHZCNZVEVIVJCEKVLUPACEQV
JCERSVKUQCULUPAUFUGTUHTVCULVBHZCOVHVBCEPVMVGCVMUMBDKVGULABDQUMB
DRSUHTUJUK $.
$}

The last one is a suggestion for the modification of your original
theorem and seems to be the same than Thierry's theorem (I don't know
how can the distinct variable conditions and the letters at the end be
different then).

Peter

[Mázsa Péter]

On Fri, Jun 16, 2017 at 8:34 AM, Mázsa Péter <pe...@mazsa.com> wrote:
> ${
> $d x y $. $d A x $. $d A y $.
> $( Partition in terms of the definition of disjointness ~ df-disj .
> (Contributed by Peter Mazsa 01-Feb-2017.) $)
> dfprt3 $p |- ( Prt A <-> A. y E* x ( x e. A /\ y e. x ) ) $=
> ( wprt cv wdisj wcel wa wmo wal dfprt2 df-disj bitri ) CDACAEZF
> NCGBENGHAIBJACKABCNLM $.
> $}

Sorry I forgot to quote this dependency: the theorem above is based on dfprt2
which connects Rodolfo Medina's df-prt and Mario's df-disj:

${
$d x y $. $d A x $. $d A y $.

$( Partition in terms of disjointness df-disj
(this theorem is a kind of justification of the concept ~ df-prt :
it demonstrates that ~ df-prt has a similar status relative to ~ df-disj
than the concept ~ df-uni relative to ~ df-iun , cf. ~ uniiun .

(Contributed by Peter Mazsa 01-Feb-2017.) $)

dfprt2 $p |- ( Prt A <-> Disj_ x e. A x ) $=
( vy wprt cv wceq cin c0 wo wral wdisj df-prt id disjor bitr4i
) BDAEZCEZFZPQGHFICBJABJABPKACBLBPQACRMNO $.
$}

Peter

[Mázsa Péter]

On Thu, Jun 15, 2017 at 7:26 PM, 'avekens' via Metamath
<meta...@googlegroups.com> wrote:
> A question to the experts:
> Are there any interesting statements about double restricted existential
> uniqueness? I searched for "E! ? e. ? E! ? e. ?" in set.mm, but I found
> nothing.
> I wonder if a theorem analogous to 2eu5 can be proven, maybe
> 2reu5 $p |- ( ( E! x e. A E! y e. B ph /\ A. x e. A E* y e. B ph ) <-> ( E.
> x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x
> = z /\ y = w ) ) ) ) $=

I'm not an expert and I don't know whether this helps, but the 2eu5
(i.e. which is analogous to eu5 in a way that it explicates 2 E!-s by
using only E.-s and E*-s) would be trivially
2reu5 $p |- ( E! x e. A E! y e. B ph <->
( E. x e. A ( E. y e. B ph /\ E* y e. B ph ) /\
E* x e. A ( E. y e. B ph /\ E* y e. B ph ) ) )
[use eu5 2 times: first use it to substitute E! y e. B with ( E. y e.
B ph /\ E* y e. B ph ), then, by substituting E! x e. A ph with
E! x e. A ( E. y e. B ph /\ E* y e. B ph ), use eu5 a second time to
get 2reu5 above].

then, based on r19.40, you may prove a theorem like
|- ( E! x e. A E! y e. B ph ->

( E. x e. A E. y e. B ph /\

E. x e. A E* y e. B ph /\
E* x e. A E. y e. B ph /\
E* x e. A E* y e. B ph ) )

Peter

[Norman Megill]

On Thursday, June 15, 2017 at 9:02:08 PM UTC-4, Thierry Arnoux wrote:

Hi,

Is the restricted "at most one" quantifier E* y e. B defined?

I have something that could be useful the in the "proba" branch:

  ${
    $d x y A $. $d x B $.
    $( A condition allowing swap of uniqueness and existential quantifiers. $)
    2reuswap2 $p |- ( A. x e. A E* y ( y e. B /\ ph ) -> ( E! x e. A E. y e. B ph -> E! y e. B E. x e. A ph ) ) $=

I am adding some basic df-rmo theorems today and hope to have them on the us2 site sometime tomorrow.  After changing E* y ( y e. B /\ ph ) to E* y e. B ph, I will adopt your 2reuswap2 (renamed to 2reuswap) in place of the present 2reuswap since it is more general.

Norm

[David A. Wheeler]

On June 16, 2017 4:34:45 PM EDT, Norman Megill <n...@alum.mit.edu> wrote:
>
>I am adding some basic df-rmo theorems today and hope to have them on
>the
>us2 site sometime tomorrow.

I think this is a good call. It makes things a little more consistent, and I like definitions that make other expressions simpler and clearer.


--- David A.Wheeler

[avekens]

Hi all,
thanks a lot for the valuable contributions to my request! Especially the hint of Thierry that the restricted "at most one" quantifier E* y e. B is not defined yet has started a good and constructive discussion. I just transformed 2eu5 to my 2reu5 and was not aware that E* y e. B was not defined...

I'll add some further remarks on some of your contributions shortly.

Best regards,
Alexander van der Vekens

[avekens]

Hi Norman,
that's really great and I appreciate very much the addition of the (missing) definition of the restricted "at most one" quantifier E* y e. B.

In the meantime, I started to prove some theorems based on df-rmo, too. It seemed to be very easy to transform the theorems for E! y e. B in section "Restricted quantification" into theorems für E* y e. B just replacing the string "eu" with "mo". Only to prove cbvrmo (analogon to cbvreu) a theorem analogous to sb8eu is required which is not available yet. But it is easy to prove:

  ${
    $d w y z $.  $d ph z w $.  $d w x z $.
    sb8mo.1 $e |- F/ y ph $.
    $( Variable substitution in uniqueness quantifier ("at most one"), analogous to ~ sb8eu .
       THEOREM SHOULD BE PLACED IN SECTION "Existential uniqueness"!
       (Contributed by Alexander van der Vekens, 17-Jun-2017.) $)
    sb8mo $p |- ( E* x ph <-> E* y [ y / x ] ph ) $=
      ( wex weu wi wsb wmo sb8e sb8eu imbi12i df-mo 3bitr4i ) ABEZABFZGABCHZCEZ
      QCFZGABIQCIORPSABCDJABCDKLABMQCMN $.
      $( [17-Jun-2017] $)
  $}

With this theorem, the proof of cbvrmo is in principle the same as for cbvreu:

  ${
    $d x z A $.  $d y z A $.  $d z ph $.  $d z ps $.
    cbvral.1 $e |- F/ y ph $.
    cbvral.2 $e |- F/ x ps $.
    cbvral.3 $e |- ( x = y -> ( ph <-> ps ) ) $.

    ...

    $( Change the bound variable of a restricted uniqueness quantifier ("at most one")
       using implicit substitution, analogous to ~ cbvreu .
       (Contributed by Alexander van der Vekens, 17-Jun-2017.) $)
    cbvrmo $p |- ( E* x e. A ph <-> E* y e. A ps ) $=
      ( vz cv wcel wa wmo wrmo wsb nfv sb8mo sban mobii df-rmo anbi1i nfsb nfan
      clelsb3 wceq eleq1 sbequ sbie syl6bb anbi12d cbvmo bitri 3bitri 3bitr4i )
      CJEKZALZCMZDJZEKZBLZDMZACENBDENUQUPCIOZIMUOCIOZACIOZLZIMZVAUPCIUPIPQVBVEI
      UOACIRSVFIJZEKZVDLZIMVAVEVIIVCVHVDICEUDUASVIUTIDVHVDDVHDPACIDFUBUCUTIPVGU
      RUEZVHUSVDBVGUREUFVJVDACDOBAIDCUGABCDGHUHUIUJUKULUMACETBDETUN $.
      $( [17-Jun-2017] $)
  $}

Maybe this helps a little bit.

[avekens]

Hi Peter,
thank you very much for your hints, I think they are good starting points for further investigations. I hope I can contribute some theorems based on your suggestions and the new definition of E* y e. B as soon as it is officially available in set.mm.

Alexander

[avekens]

Hi all,
it took several hours, but I was able to proof my stated 2reu5 in a slightly modified form:

2reu5 $p |- ( ( E! x e. A E! y e. B ph /\ A. x e. A E* y e. B ph )

                  <-> ( E. x e. A E. y e. B ph /\ E. z E. w A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) )  $=

The difference is the quantifiers for z and w (E. z E. w instead of E. z e. A E. w e. B). However, I am confident that my original theorem (see below) can also be proven (I guess some renaming of variables will be necessary).

I put the proof and the required lemmas into the attachment (which also contains some theorems for the new df-rmo definition, some of them I needed for the proof of 2reu5!). Maybe this will find its way into set.mm ..

Best regards, and have a nice (rest of the) weekend,
Alexander

Am Donnerstag, 15. Juni 2017 19:26:06 UTC+2 schrieb avekens:

[Norman Megill]

Hi Alexander,

Good work!

df-rmo and some of the theorems in your attachment were added to set.mm (develop commit 3da3911) yesterday.
http://us2.metamath.org:8888/mpeuni/mmrecent.html
Perhaps you can rework this to use the ones in the current set.mm?  Then I will add your new ones to set.mm.

I will probably be adding a handful of additional df-rmo helper theorems today or tomorrow as needed to incorporate df-rmo into existing proofs.  So maybe wait a couple of days before updating your attachment.  I'll post a notice here when I'm done.

Norm

[Norman Megill]

On Saturday, June 17, 2017 at 12:26:27 PM UTC-4, Norman Megill wrote:

Hi Alexander,

Good work!

df-rmo and some of the theorems in your attachment were added to set.mm (develop commit 3da3911) yesterday.
http://us2.metamath.org:8888/mpeuni/mmrecent.html
Perhaps you can rework this to use the ones in the current set.mm?  Then I will add your new ones to set.mm.

I will probably be adding a handful of additional df-rmo helper theorems today or tomorrow as needed to incorporate df-rmo into existing proofs.  So maybe wait a couple of days before updating your attachment.  I'll post a notice here when I'm done.

I'm done with the df-rmo update.  It is on us2 and in develop commit 1f5ae48.

Norm

[Alexander van der Vekens]

Thanks, Norman.

In the meantime, I could prove my original assumption/theorem reu5! I'll providemy material after I consolidated it with the updates for df-rmo. I hope I can finish this next weekend.

Alexander

[David A. Wheeler]

On Sun, 18 Jun 2017 10:31:57 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> > df-rmo and some of the theorems in your attachment were added to set.mm
> > (develop commit 3da3911) yesterday.
> > http://us2.metamath.org:8888/mpeuni/mmrecent.html

> > <http://www.google.com/url?q=http%3A%2F%2Fus2.metamath.org%3A8888%2Fmpeuni%2Fmmrecent.html&sa=D&sntz=1&usg=AFQjCNH747WC0VSilsFY9CVrk5C6gvK44Q>

> > Perhaps you can rework this to use the ones in the current set.mm? Then
> > I will add your new ones to set.mm.
> >
> > I will probably be adding a handful of additional df-rmo helper theorems
> > today or tomorrow as needed to incorporate df-rmo into existing proofs. So
> > maybe wait a couple of days before updating your attachment. I'll post a
> > notice here when I'm done.
> >
>
> I'm done with the df-rmo update. It is on us2 and in develop commit
> 1f5ae48.

I looked at this page:
http://us2.metamath.org:88/mpegif/mmrecent.html

and didn't see a note of df-rmo and friends. Is that just not posted yet?

--- David A. Wheeler

[Norman Megill]

On Sunday, June 18, 2017 at 7:32:31 PM UTC-4, David A. Wheeler wrote:

On Sun, 18 Jun 2017 10:31:57 -0700 (PDT), Norman Megill wrote:

> I'm done with the df-rmo update.  It is on us2 and in develop commit
> 1f5ae48.

I looked at this page:
  http://us2.metamath.org:88/mpegif/mmrecent.html

and didn't see a note of df-rmo and friends.  Is that just not posted yet?

It has been posted for 7 hours now.  Maybe try a browser refresh?  There are 40+ new and revised theorems, everything since 16-Jul-2017, so you have to look at a "1000 most recent" page to see all of them.

Norm

[Alexander van der Vekens]

Hi Norman,
I got set.mm (develop commit 1f5ae48) via http://us2.metamath.org:8888/mpeuni/mmrecent.html and reworked my proofs accordingly (and removed duplicates).

In section "Restricted quantification", there are theorems for E* analogous to theorems for E!. Maybe you can put these next to the corresponding theorems for E!

In section "The universal class" are theorems for double restricted quantifiers. In my previous contribution, I used short names, calling the theorems 2reu5a, 2reu5b ,2reu5c, 2reu5a, because I used them as lemmas for my 2reu5. But as I saw that the numbering is not consistent (2reu5 is analogous to ~ 2eu5 and ~ reu3 , so it could also have been named 2reu3), I renamed my theorems to reflect their contents, but resulting in rather long names.

So the two attached files differ only in the used names: in avrmo.mm, the short names are used, in avrmo_ln.mm the long names.  Maybe you can decide which variant should be taken for set.mm, or even invent completely new names.

Alexander

Am Sonntag, 18. Juni 2017 19:31:57 UTC+2 schrieb Norman Megill:

[Alexander van der Vekens]

Ups, I missed one duplicate: my theorem rmoim is identical with theorem imrmo contained in the latest set.mm! So rmoim can be removed, and its usage in proofs (for theorems rmoimia and rmoreximralrmo/2rmorex) can be replaced by imrmo.

[Norman Megill]

On Thursday, June 22, 2017 at 4:53:01 PM UTC-4, Alexander van der Vekens wrote:

Hi Norman,
I got set.mm (develop commit 1f5ae48) via http://us2.metamath.org:8888/mpeuni/mmrecent.html and reworked my proofs accordingly (and removed duplicates).

In section "Restricted quantification", there are theorems for E* analogous to theorems for E!. Maybe you can put these next to the corresponding theorems for E!

In section "The universal class" are theorems for double restricted quantifiers. In my previous contribution, I used short names, calling the theorems 2reu5a, 2reu5b ,2reu5c, 2reu5a, because I used them as lemmas for my 2reu5.

These are now on the us2 server (see http://us2.metamath.org:88/mpeuni/mmrecent1000.html)

I created a mathbox for you which will provide you with an independent section for you to work on your theorems, and in the future you can send me revisions to your mathbox.  This way your theorems can be added to set.mm immediately and "curated" later as we decide which should go into the main set.mm and where.  Most contributors send me periodic updates to their mathboxes, which makes things a little easier for me.

I put most of your theorems in an appropriate place in the main part of set.mm, but I left 2 of them in your mathbox.  One of them, rmoimi, is a 1-step weakening of rmoimia, and we would ordinarily include it only if it was used enough to result in a net reduction in set.mm size (such as with reximi that is used over 100 times).  The other one, 2reu5a, will probably never be used, and its derivation is basically just substituting reu5 twice.  These were my subjective judgment calls of course, and if they are needed in the future, they can be imported into the main set.mm from your mathbox.

Actually, while I think they are interesting, it is unlikely that any of the 2reu* theorems will be used very often.  The original 2eu* theorems have never been of any use except to prove variations of themselves.  I included them to show what I thought were non-obvious properties of double E! and E* compared to double E., particularly since the literature has been wrong.

For your rmoim* theorems, I swapped ph and ps to be consistent with moim* and others.  For example, in con3i we show "ph -> ps" implies "-. ps -> -. ph", making the reversal more prominent (to me at least) since the conclusion is typically the first thing we look at in a theorem.
 

But as I saw that the numbering is not consistent (2reu5 is analogous to ~ 2eu5 and ~ reu3 , so it could also have been named 2reu3), I renamed my theorems to reflect their contents, but resulting in rather long names.

So the two attached files differ only in the used names: in avrmo.mm, the short names are used, in avrmo_ln.mm the long names.  Maybe you can decide which variant should be taken for set.mm, or even invent completely new names.

I think shorter names are usually easier to remember, as long as they are chosen carefully to conform to some convention, and they require less typing.  For example, the long label 2reubirexrmo doesn't completely reflect its contents, since it doesn't describe all 8 quantifiers nor the conjunctions.  To do that would of course result in a very long name.  But for a long partial description it can be hard to remember which parts are described and which are omitted, especially if they haven't been looked at in a while.

While 2reubirexrmo's short name 2reu5a probably isn't ideal, it does let us know that it is in the "2reu" family, which is the most important thing, so we can browse the "2reu*" theorems to see if one is of interest.  The "5a" by itself isn't meaningful, but since we have 2eu5 and 2reu5, the "a" indicates a variation.  Most importantly, I can remember 2reu5a more easily than 2reubirexrmo.  In the end, though, choosing names is more of an art than a science.

You are right that there should be better consistency in the *eu* and *mo* naming.  I already changed immo* to moim* and will look at others.  As you can see at the top of set.mm, we have made many name changes over the years to achieve better consistency.

Norm
 

[Norman Megill]

On Sunday, June 25, 2017 at 12:07:42 PM UTC-4, Alexander van der Vekens wrote:

Ups, I missed one duplicate: my theorem rmoim is identical with theorem imrmo contained in the latest set.mm! So rmoim can be removed, and its usage in proofs (for theorems rmoimia and rmoreximralrmo/2rmorex) can be replaced by imrmo.

No problem, I already took care of that.

Norm

[Alexander van der Vekens]

Thanks, Norman - you have put a lot of work in this topic. I will have a closer look at it in the next days, and continue my work based on your enhancements of set.mm.
I think we can close this discussion thread now (from my point of view). I have in mind to use the double (restricted) existential uniqueness in the context of operations (sort of "E! x e. A E! y e. B ( x F y ) = ...") - I will inform you when I obtained any valuable results.

Regards,
Alexander

[Alexander van der Vekens]

Hi all,
after I proved 2reu5 some days before I tried to prove analogs to 2eu1 up to 2eu8 for double restricted existential uniqueness. Except for 2eu6, I was successful - you can find the results in my mathbox (attached to this post).

• Technical remark: I created a pull request (#124) for my changed mathbox from my own repository, but it failed: on calling "verify proof *" in the metamath program, I get the "Warning:  The following $p statement(s) were not proved:  2reurex". But looking at 2reurex with "show proof 2reurex" everything looks fine. Can anybody tell me the reason for this warning? Maybe someone can have a look at my Pull Request #124 because of the additional errors I get...
  

I tried to prove something similar to 2eu6, but I didn't find anything useful. Since 2eu6 is not used in any proof within set.mm, I stopped investigating here.

To prove 2reu1 up to 2reu8, some other theorems similar to already existing ones were required - these are also contained im my mathbox. Hopefully, 2reu1 up to 2reu8 and the supporting theorems can be moved to the main part of set.mm somehow.

Regards,
Alexander

[Norman Megill]

Hi Alexander,

Your proof of 2reurex is not complete, as you can see from ?s in the compressed proof:
...CEFUMUOA??KUMUPUNC...

If you do this:
MM> prove reurex
MM-PA> show new_proof/all/unknown
 87            vx=?              $? set x e. A
 88            vy=?              $? set y e. B

It is asking to prove that x e. A is a set, which can't be done.  That's why it is incomplete.

If you look further:
 89       syl5bi.1=excom    $p |- ( E. x e. A E. y e. B ph <-> E. y e. B E. x
                                                                      e. A ph )

You are using excom.  If you delete step 89 and assign it to rexcom, 'improve all' will complete the proof.

The reason "show proof" shows all steps completed is that it suppresses the syntax-building steps, which you need /all to show.

The mmj2 program handles syntax in a different way and would not let you assign excom to step 89 in the first place.  MM-PA is designed to tolerate "non-grammatical" syntax that the language allows in its most general form, whereas mmj2 restricts things to the grammar the we use in set.mm and 99% of all other Metamath uses.  (There some improvements I have planned for MM-PA to solve some of these issues, but it will be a while before that happens.)  You may want to try mmj2.

Norm

[Alexander van der Vekens]

Ah, OK - I see. Thanks, Norman, for this hint.
I'll correct this and try again to pull after I have fixed this.

Alexander