Equivalent forms of the axiom of replacement

[jkingdon]

The comment for https://us.metamath.org/mpeuni/f1dmex.html says "This theorem is equivalent to the Axiom of Replacement". Is there is a way to formalize this statement?

First of all, we'd want, I suppose, a notation REP analogous to CHOICE ( https://us.metamath.org/mpeuni/df-ac.html ) or EXMID ( https://us.metamath.org/ileuni/df-exmid.html ).

But how to state the theorem in such a way that it would imply REP?

f1dmex is (𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V . The class B isn't much of a problem, it could be replaced by a universally quantified set variable which is similar to what we do in other similar circumstances. But what about A? It has to be a class which is not a priori constrained to be a set, as that's the whole point. Perhaps we can refer to ( `' F " B ) (not that I looked carefully at whether replacement would be needed to make that notation express what we want it to express)? Perhaps there is some other solution?

Inspired by the Mastodon thread at https://mathstodon.xyz/@highergeometer/113480205427072831 which isn't about the exact same ax-rep equivalence as f1dmex but is about one which is pretty similar.

[jkingdon]

I think maybe I have a statement of it. This isn't correct; see below

f1dmexr.1 $e |- ( A. f A. b ( f : dom f -1-1-> b ) -> dom f e. _V ) $.
f1dmexr $p |- |- ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y
      <-> E. w ( w e. x /\ A. y ph ) ) ) $= ... $.
$( $j usage 'f1dmexr' avoids 'ax-rep' ; $)

(this is without trying to define a REP notation; the version with that notation would just replace the conclusion with REP).

[benjub]

To formalize equivalences, we do not have to introduce new notation. For instance, we proved several equivalents, labeled axrep?, without new notation.

Your f1dmexr.1 does not formalize REP: it is true without REP, since f is a set function.

I think proving axrep from all the other axioms plus f1dmex would qualify as a proof that f1dmex is equivalent to ax-rep.

[jkingdon]

Your f1dmexr.1 does not formalize REP: it is true without REP, since f is a set function.

Oh, you're right. This attempt accidentally excludes the possibility of F as a proper class, so it doesn't work.

I think proving axrep from all the other axioms plus f1dmex would qualify as a proof that f1dmex is equivalent to ax-rep.

Hmm, like this?

f1dmexr2.1 $e |- ( ( F : A -1-1-> B /\ B e. C ) -> A e. _V ) $.
f1dmexr2 $p |- |- ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y
      <-> E. w ( w e. x /\ A. y ph ) ) ) $= ... $.
$( $j usage 'f1dmexr2' avoids 'ax-rep' ; $)

This doesn't seem to provide a fully flexible f1dmex. That is, you could satisfy the hypothesis by simply substituting in (/) for A.

Or maybe you'd need

f1dmexr3ax $a |- ( ( F : A -1-1-> B /\ B e. C ) -> A e. _V ) $.
f1dmexr3 $p |- |- ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y
      <-> E. w ( w e. x /\ A. y ph ) ) ) $= ... $.
$( $j usage 'f1dmexr3' avoids 'ax-rep' ; $)

which I guess might work but I can't find a lot of examples of this technique so I'm not sure what to think.

[sctfn]

I don't think you can state a single formula that is equivalent to REP in ZFC. If you could, then you could finitely axiomatize ZFC (by just stating REP as an axiom). We know that's not possible (that's the whole reason for NBG), so I don't think it's doable.

[benjub]

Sorry, I was not clear. What I meant is much more low tech: I think we should be content with a theorem and comment like

($ Prove ~ax-rep from ~f1dmex and earlier axioms.  Note that the only use of ~ ax-rep is via f1dmex .$)
axrep9 $p |- ...

which we already do in a few instances in set.mm.

@sctfn is right that you cannot in general have such a REP (although beware that we have the axiom scheme of separation ax-sep, so your argument is correct if we do not use ax-sep either (it's probably true if you allow it too, but with a more involved argument)).

In this specific case, however, if your proof uses only a known finite number of instances of the scheme f1dmex, then you can put these specific instances as $e-hypotheses.

[jkingdon]

if your proof uses only a known finite number of instances of the scheme f1dmex, then you can put these specific instances as $e-hypotheses.

Seems like that's what we'd need to do.