Add constructible set definitions to mathbox

[BTernaryTau]

This pull request follows the construction of the constructible universe carried out in [TakeutiZaring]. It also adds definitions for ordinals 5 through 9, and it moves df-bj-mpt3 into main. No theorems are included, though I am already working on some.

[avekens]

Please do not move df-bj-mpt3 yet/in this PR, but only if it is used by you, and/or some basic theorems are available.

[BTernaryTau]

Please do not move df-bj-mpt3 yet/in this PR, but only if it is used by you, and/or some basic theorems are available.

Does using it in the definitions for ~F and _J not count? Those two are what forced me to move it in this PR.

[avekens]

Please do not move df-bj-mpt3 yet/in this PR, but only if it is used by you, and/or some basic theorems are available.

Does using it in the definitions for ~F and _J not count? Those two are what forced me to move it in this PR.

Oh yes, I see! I only searched for "cmpt3" and did not find it, because there are no theorems using it.
But since there are no theorems using this definition, it is not clear to me if it is "sound", i.e., really defines what is expected. Especially because the definition is conceptually different from those for 1 (df-mpt) resp. 2 (df-mpo) arguments, e.g.:

df-mpo $a |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } $.

So why not define df-mpt3 as follows:

df-mp3 $a |- ( x e. A , y e. B , z e. C |-> D ) = { <. <. x , y , z >. , d >. | ( ( x e. A /\ y e. B  /\ z e. C ) /\ d = D ) } $.

Would this definition be equivalent with df-bj-mpt3? If it is, this should be provided as theorem (at least this one).
Maybe some other theorems may be added, corresponding to df-mpo, e.g., ~mpofun, ~rnmpo, ~reldmmpo, etc.

Finally, I expect ~bj-mpt3mpt to be proven and then moved as ~mpt3mpt to main:

  @( Express a three-argument function as a one-argument function, or
     vice-versa.  Similar to ~ mpompt .  @)
  bj-mpt3mpt $p |- ( t e. ( A X. B X. C ) |-> D ) =
                                          ( x e. A , y e. B , z e. C |-> E ) $=
    ? $.

@benjub what do you think?

[BTernaryTau]

So why not define df-mpt3 as follows:

That actually was my original approach (see 57dd82b), though I had to use { <. <. <. w , x >. , y >. , z >. | ph } instead of { <. <. w , x , y >. , z >. | ph } because the latter caused a parsing error. I only switched away from that after realizing that df-bj-mpt3 already existed, but I'm fine with going back to the original approach as long as we can agree on how to deal with df-bj-mpt3 (maybe comment it out alongside bj-mpt3mpt until we have the prerequisites to prove it as a theorem?)

[benjub]

A reason for not using the proposed df-mp3 is the parsing error @BTernaryTau discovered. I wrote https://us.metamath.org/mpeuni/df-bj-mpt3.html that way to introduce as little new syntax as possible.

As for said parsing error, see for instance the second paragraph of https://groups.google.com/g/metamath/c/VAGNmzFkHCs/m/bzSyeHdEieUJ

Feel free to use the commented out bj-mpt3mpt to update the proof (and the credits to you, of course).

It is only fitting that ternary functions are moved to the main section by @BTernaryTau.

[avekens]

OK, for df-mpo, we need (and have) df-oprab, but we do not have a definition of { <. <. x , y , z >. , a >. | ph }, which would be required for my proposed defintion of df-mpo. Therefore, it is OK to take df-bj-mpt3 and move it as df-mpt3 to main. I would still like to see, however, the proof of bj-mpt3mpt, which can be moved as mpt3mpt to main, too.

[BTernaryTau]

It is only fitting that ternary functions are moved to the main section by @BTernaryTau.

Now all I need is an excuse to move taupi into main.

I would still like to see, however, the proof of bj-mpt3mpt, which can be moved as mpt3mpt to main, too.

Added.

[BTernaryTau]

Anything else to resolve before this can be merged?