Here is a challenge, some basic math:
"The image of a non empty domain is non empty"

Or formally, s≠0 stands for EXIST(c):[c e s]:

ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]

The above is provable in ZF, right?
I doubt it can be proved in DC Proof.

P.S.: Was using the weaker form ALL(x):[x e a => f(x) e b]
instead of ALL(x):[x e a <=> f(x) e b], strictly the image

f[a] would be only that b with ALL(x):[x e a <=> f(x) e b].
But lets see whether the simpler can be proved?

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:57:25 UTC+1:
> Here is a challenge, some basic math:
> "The image of a non empty domain is non empty"
>
> Or formally, s≠0 stands for EXIST(c):[c e s]:
>
> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
>
> The above is provable in ZF, right?
> I doubt it can be proved in DC Proof.

Corr.:
Oh my, the stronger would be ALL(y):[y e b <=> EXIST(x):[x e a & f(x)=y]]
Anyway lets stick to the problem with the weaker, which would say:
"The image of a non empty set is contained in a non empty set"

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 03:00:27 UTC+1:
> P.S.: Was using the weaker form ALL(x):[x e a => f(x) e b]
> instead of ALL(x):[x e a <=> f(x) e b], strictly the image
>
> f[a] would be only that b with ALL(x):[x e a <=> f(x) e b].
> But lets see whether the simpler can be proved?
> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:57:25 UTC+1:
> > Here is a challenge, some basic math:
> > "The image of a non empty domain is non empty"
> >
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> >
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> >
> > The above is provable in ZF, right?
> > I doubt it can be proved in DC Proof.

See my proof at your identical posting at sci.logic.

On Tuesday, November 23, 2021 at 8:57:25 PM UTC-5, Mostowski Collapse wrote:
> Here is a challenge, some basic math:
> "The image of a non empty domain is non empty"
>
> Or formally, s≠0 stands for EXIST(c):[c e s]:
>
> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
>
> The above is provable in ZF, right?
> I doubt it can be proved in DC Proof.

There is a second error. Your existence quantifier is wrongly
placed or missing. You dont have EXIST(z) anywhere
after the implication sign =>:

7 ALL(x):ALL(f):ALL(y):ALL(z):[ALL(a):[a in x => f(a) in y]
& EXIST(a):a in x
& ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]]
=> EXIST(a):a in z]
Conclusion, 1

You did not prove what I wrote:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> Or formally, s≠0 stands for EXIST(c):[c e s]:
> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

The above is provable in FOL+ZF.
It is not provable in DC Proof alone.

Dan Christensen schrieb am Mittwoch, 24. November 2021 um 14:56:39 UTC+1:
> See my proof at your identical posting at sci.logic.
> On Tuesday, November 23, 2021 at 8:57:25 PM UTC-5, Mostowski Collapse wrote:
> > Here is a challenge, some basic math:
> > "The image of a non empty domain is non empty"
> >
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> >
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> >
> > The above is provable in ZF, right?
> > I doubt it can be proved in DC Proof.

See my reply to your identical claim at sci.logic just now.

Dan

On Wednesday, November 24, 2021 at 9:13:35 AM UTC-5, Mostowski Collapse wrote:
> There is a second error. Your existence quantifier is wrongly
> placed or missing. You dont have EXIST(z) anywhere
> after the implication sign =>:
>
....

I don't want to prove something from Wikipedia.
It doesn't have an english phrasing, its just a formula.
The full english phrasing would be:

- For every non empty set
there exists a set
that is a super set of an image of the former set
and that is non empty

So the task is to prove this theorem:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> Or formally, s≠0 stands for EXIST(c):[c e s]:
> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

Dan Christensen schrieb am Mittwoch, 24. November 2021 um 17:20:44 UTC+1:
> See my reply to your identical claim at sci.logic just now.
>
> Dan
> On Wednesday, November 24, 2021 at 9:13:35 AM UTC-5, Mostowski Collapse wrote:
> > There is a second error. Your existence quantifier is wrongly
> > placed or missing. You dont have EXIST(z) anywhere
> > after the implication sign =>:
> >
> ...

In the case of DC Proof, you possibly want a closed
higher order formula, so it would be:

ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[ALL(x):[x e a => f(x) e b] & EXIST(c):[c e b]]]

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 17:32:03 UTC+1:
> I don't want to prove something from Wikipedia.
> It doesn't have an english phrasing, its just a formula.
> The full english phrasing would be:
>
> - For every non empty set
> there exists a set
> that is a super set of an image of the former set
> and that is non empty
>
> So the task is to prove this theorem:
> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ
> Dan Christensen schrieb am Mittwoch, 24. November 2021 um 17:20:44 UTC+1:
> > See my reply to your identical claim at sci.logic just now.
> >
> > Dan
> > On Wednesday, November 24, 2021 at 9:13:35 AM UTC-5, Mostowski Collapse wrote:
> > > There is a second error. Your existence quantifier is wrongly
> > > placed or missing. You dont have EXIST(z) anywhere
> > > after the implication sign =>:
> > >
> > ...

You can also switch sides of the conjunction &:

ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[EXIST(c):[c e b] & ALL(x):[x e a => f(x) e b]]]

Then the phrasing is a little shorter, using bounded quantifier phrasing twice:

- For every non empty set
there exists an non empty set
that is a super set of an image of the former set

You can also phrase the ALL(f) quantifier:

- For every function and for every non empty set
there exists an non empty set
that is a super set of the function image of the former set
Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 17:34:18 UTC+1:
> In the case of DC Proof, you possibly want a closed
> higher order formula, so it would be:
>
> ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[ALL(x):[x e a => f(x) e b] & EXIST(c):[c e b]]]
> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 17:32:03 UTC+1:
> > I don't want to prove something from Wikipedia.
> > It doesn't have an english phrasing, its just a formula.
> > The full english phrasing would be:
> >
> > - For every non empty set
> > there exists a set
> > that is a super set of an image of the former set
> > and that is non empty
> >
> > So the task is to prove this theorem:
> > Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> > https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ
> > Dan Christensen schrieb am Mittwoch, 24. November 2021 um 17:20:44 UTC+1:
> > > See my reply to your identical claim at sci.logic just now.
> > >
> > > Dan
> > > On Wednesday, November 24, 2021 at 9:13:35 AM UTC-5, Mostowski Collapse wrote:
> > > > There is a second error. Your existence quantifier is wrongly
> > > > placed or missing. You dont have EXIST(z) anywhere
> > > > after the implication sign =>:
> > > >
> > > ...

On Wednesday, November 24, 2021 at 11:34:18 AM UTC-5, Mostowski Collapse wrote:
> In the case of DC Proof, you possibly want a closed
> higher order formula, so it would be:
>
> ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[ALL(x):[x e a => f(x) e b] & EXIST(c):[c e b]]]

It seems you have truly caught the Muckenheim disease, Jan Burse. That's not basic math. It's basic nonsense. Get back to us when you are feeling better.

Dan

Well its basic math. Its a basic theorem, because
its a simple theorem. It uses only some simple notions:
- non empty set
- image by a function

It would be non-basic math, aka advanced math, if
the theorem were more complex.

The theorem can be proved in FOL+ZF.
But it cannot be proved in DC Proof.

Do you know why?

Dan Christensen schrieb am Mittwoch, 24. November 2021 um 19:09:55 UTC+1:
> On Wednesday, November 24, 2021 at 11:34:18 AM UTC-5, Mostowski Collapse wrote:
> > In the case of DC Proof, you possibly want a closed
> > higher order formula, so it would be:
> >
> > ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[ALL(x):[x e a => f(x) e b] & EXIST(c):[c e b]]]
> It seems you have truly caught the Muckenheim disease, Jan Burse. That's not basic math. It's basic nonsense. Get back to us when you are feeling better.
>
> Dan

Here is a tableaux proof of the theorem in FOL+ZF, using Exy for x e y:

∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) → ∀a(∃zEza → ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b))) is valid.
https://www.umsu.de/trees

The LHS is an instance of the axiom schema of replacement from ZF.

Woa! Thats quite amazing that trees can find it.

Mostowski Collapse schrieb am Donnerstag, 25. November 2021 um 00:03:28 UTC+1:
> Well its basic math. Its a basic theorem, because
> its a simple theorem. It uses only some simple notions:
> - non empty set
> - image by a function
>
> It would be non-basic math, aka advanced math, if
> the theorem were more complex.
>
> The theorem can be proved in FOL+ZF.
> But it cannot be proved in DC Proof.
>
> Do you know why?
> Dan Christensen schrieb am Mittwoch, 24. November 2021 um 19:09:55 UTC+1:
> > On Wednesday, November 24, 2021 at 11:34:18 AM UTC-5, Mostowski Collapse wrote:
> > > In the case of DC Proof, you possibly want a closed
> > > higher order formula, so it would be:
> > >
> > > ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[ALL(x):[x e a => f(x) e b] & EXIST(c):[c e b]]]
> > It seems you have truly caught the Muckenheim disease, Jan Burse. That's not basic math. It's basic nonsense. Get back to us when you are feeling better.
> >
> > Dan

See my reply to your identical posting at sci.logic just now.

Dan

On Wednesday, November 24, 2021 at 6:03:28 PM UTC-5, Mostowski Collapse wrote:
> Well its basic math. Its a basic theorem, because
> its a simple theorem. It uses only some simple notions:
> - non empty set
> - image by a function
>
> It would be non-basic math, aka advanced math, if
> the theorem were more complex.
>
> The theorem can be proved in FOL+ZF.
> But it cannot be proved in DC Proof.
>
> Do you know why?
> Dan Christensen schrieb am Mittwoch, 24. November 2021 um 19:09:55 UTC+1:
> > On Wednesday, November 24, 2021 at 11:34:18 AM UTC-5, Mostowski Collapse wrote:
> > > In the case of DC Proof, you possibly want a closed
> > > higher order formula, so it would be:
> > >
> > > ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[ALL(x):[x e a => f(x) e b] & EXIST(c):[c e b]]]
> > It seems you have truly caught the Muckenheim disease, Jan Burse. That's not basic math. It's basic nonsense. Get back to us when you are feeling better.
> >
> > Dan

You didn't prove what was required.

Dan Christensen schrieb am Donnerstag, 25. November 2021 um 04:22:32 UTC+1:
> See my reply to your identical posting at sci.logic just now.
>
> Dan
> On Wednesday, November 24, 2021 at 6:03:28 PM UTC-5, Mostowski Collapse wrote:
> > Well its basic math. Its a basic theorem, because
> > its a simple theorem. It uses only some simple notions:
> > - non empty set
> > - image by a function
> >
> > It would be non-basic math, aka advanced math, if
> > the theorem were more complex.
> >
> > The theorem can be proved in FOL+ZF.
> > But it cannot be proved in DC Proof.
> >
> > Do you know why?
> > Dan Christensen schrieb am Mittwoch, 24. November 2021 um 19:09:55 UTC+1:
> > > On Wednesday, November 24, 2021 at 11:34:18 AM UTC-5, Mostowski Collapse wrote:
> > > > In the case of DC Proof, you possibly want a closed
> > > > higher order formula, so it would be:
> > > >
> > > > ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[ALL(x):[x e a => f(x) e b] & EXIST(c):[c e b]]]
> > > It seems you have truly caught the Muckenheim disease, Jan Burse. That's not basic math. It's basic nonsense. Get back to us when you are feeling better.
> > >
> > > Dan

Just recall what Russell said about "the X is Y".
You translate it again into "some X is Y":

ALL(z):[ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] => EXIST(a):a in z]]

Can be vacously true if there is no z that is the
image. So you didn't learn anything from "the bald king"
example? Still doing the same errors? Just

think how "the image is translated". If you really
want to translate the english definite description,
you would need to use the strong:

EXISTUNIQUE(z):[ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] & EXIST(a):a in z]]

I offered you the weaker EXIST instead EXISTUNIQUE:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> Or formally, s≠0 stands for EXIST(c):[c e s]:
> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

But you wont be able to prove either in DC Proof. You
wont be able to prove the EXIST nor the EXISTUNIQUE
without extra axioms. Like you showed your inability to

grasp the translation of Russells "the X is Y" in theory. Also
in practice for basic math, you insist on utter nonsense
allowing for vacouse truth, instead of

make a proper existence proof.

Whats wrong with you?

Mostowski Collapse schrieb am Donnerstag, 25. November 2021 um 08:23:51 UTC+1:
> You didn't prove what was required.
> Dan Christensen schrieb am Donnerstag, 25. November 2021 um 04:22:32 UTC+1:
> > See my reply to your identical posting at sci.logic just now.
> >
> > Dan
> > On Wednesday, November 24, 2021 at 6:03:28 PM UTC-5, Mostowski Collapse wrote:
> > > Well its basic math. Its a basic theorem, because
> > > its a simple theorem. It uses only some simple notions:
> > > - non empty set
> > > - image by a function
> > >
> > > It would be non-basic math, aka advanced math, if
> > > the theorem were more complex.
> > >
> > > The theorem can be proved in FOL+ZF.
> > > But it cannot be proved in DC Proof.
> > >
> > > Do you know why?
> > > Dan Christensen schrieb am Mittwoch, 24. November 2021 um 19:09:55 UTC+1:
> > > > On Wednesday, November 24, 2021 at 11:34:18 AM UTC-5, Mostowski Collapse wrote:
> > > > > In the case of DC Proof, you possibly want a closed
> > > > > higher order formula, so it would be:
> > > > >
> > > > > ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[ALL(x):[x e a => f(x) e b] & EXIST(c):[c e b]]]
> > > > It seems you have truly caught the Muckenheim disease, Jan Burse. That's not basic math. It's basic nonsense. Get back to us when you are feeling better.
> > > >
> > > > Dan

Because you didn't understand Russells "the X is Y",
you keep continuing proving "some X is Y" nonsense.
Latest example "some Dedekind is Peano".

It even seems your DC proof tool is made to prove
such nonsense. You are totally inable to prove the
existence of omega from some foundation.

But the example I gave litterally can be even proved
from an other tool that doesn't need download and
that even works for the macintosh:

> Here is a tableaux proof of the theorem in FOL+ZF, using Exy for x e y:
> ∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) → ∀a(∃zEza → ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b))) is valid.
> https://www.umsu.de/trees
> The LHS is an instance of the axiom schema of replacement from ZF.

The axiom schema of replacement was introduce
by Abraham Fraenkel, the F in ZF signifies this axiom
schema. Its quite a powerful axiom schema.

https://en.wikipedia.org/wiki/Axiom_schema_of_replacement

To make a proper proof we would also need to
prove that f(y)=x is a definite description, namely
that we also have:

ALL(y):EXISTUNIQUE(x):f(y)=x

Only then we are allowed to apply the axiom
schema. But the above is left as an exercise.

Mostowski Collapse schrieb am Donnerstag, 25. November 2021 um 08:34:07 UTC+1:
> Just recall what Russell said about "the X is Y".
> You translate it again into "some X is Y":
>
> ALL(z):[ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] => EXIST(a):a in z]]
>
> Can be vacously true if there is no z that is the
> image. So you didn't learn anything from "the bald king"
> example? Still doing the same errors? Just
>
> think how "the image is translated". If you really
> want to translate the english definite description,
> you would need to use the strong:
>
> EXISTUNIQUE(z):[ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] & EXIST(a):a in z]]
>
> I offered you the weaker EXIST instead EXISTUNIQUE:
> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ
>
> But you wont be able to prove either in DC Proof. You
> wont be able to prove the EXIST nor the EXISTUNIQUE
> without extra axioms. Like you showed your inability to
>
> grasp the translation of Russells "the X is Y" in theory. Also
> in practice for basic math, you insist on utter nonsense
> allowing for vacouse truth, instead of
>
> make a proper existence proof.
>
> Whats wrong with you?
> Mostowski Collapse schrieb am Donnerstag, 25. November 2021 um 08:23:51 UTC+1:
> > You didn't prove what was required.
> > Dan Christensen schrieb am Donnerstag, 25. November 2021 um 04:22:32 UTC+1:
> > > See my reply to your identical posting at sci.logic just now.
> > >
> > > Dan
> > > On Wednesday, November 24, 2021 at 6:03:28 PM UTC-5, Mostowski Collapse wrote:
> > > > Well its basic math. Its a basic theorem, because
> > > > its a simple theorem. It uses only some simple notions:
> > > > - non empty set
> > > > - image by a function
> > > >
> > > > It would be non-basic math, aka advanced math, if
> > > > the theorem were more complex.
> > > >
> > > > The theorem can be proved in FOL+ZF.
> > > > But it cannot be proved in DC Proof.
> > > >
> > > > Do you know why?
> > > > Dan Christensen schrieb am Mittwoch, 24. November 2021 um 19:09:55 UTC+1:
> > > > > On Wednesday, November 24, 2021 at 11:34:18 AM UTC-5, Mostowski Collapse wrote:
> > > > > > In the case of DC Proof, you possibly want a closed
> > > > > > higher order formula, so it would be:
> > > > > >
> > > > > > ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[ALL(x):[x e a => f(x) e b] & EXIST(c):[c e b]]]
> > > > > It seems you have truly caught the Muckenheim disease, Jan Burse. That's not basic math. It's basic nonsense. Get back to us when you are feeling better.
> > > > >
> > > > > Dan

And Lazy-O-Matik, why didn't you prove:

EXIST(z):ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] ?

Too lazy to invoke your own DC Proof subset axiom?

LMAO!

On Thursday, November 25, 2021 at 2:54:56 AM UTC-5, Mostowski Collapse wrote:
>... why didn't you prove:
>
> EXIST(z):ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] ?
>

I am not deriving every result of modern set theory. Just, as you requested that, "The image of a non-empty domain is non empty." The notion of the image of a domain of a function would seem to be a given.

> Too lazy to invoke your own DC Proof subset axiom?
>

You seem to be getting more desperate by the hour, Jan Burse. Maybe you should take a little offline vacation to ponder the worrisome direction your life has taken of late.

Dan

My theorem doen't work with <=>:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> Or formally, s≠0 stands for EXIST(c):[c e s]:
> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

It is still not poved by DC Proof.

Dan Christensen schrieb am Donnerstag, 25. November 2021 um 17:31:45 UTC+1:
> On Thursday, November 25, 2021 at 2:54:56 AM UTC-5, Mostowski Collapse wrote:
> >... why didn't you prove:
> >
> > EXIST(z):ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] ?
> >
> I am not deriving every result of modern set theory. Just, as you requested that, "The image of a non-empty domain is non empty." The notion of the image of a domain of a function would seem to be a given.
> > Too lazy to invoke your own DC Proof subset axiom?
> >
> You seem to be getting more desperate by the hour, Jan Burse. Maybe you should take a little offline vacation to ponder the worrisome direction your life has taken of late.
>
> Dan

Still struggling?

You are confusing the axiom with what I want to prove.
What I want to prove has no <=>. It has only =>.
You know proofs start with axioms and then end with
what one wants to prove. Then one can say Heureka, Q.E.D.

There is still no Heureka, Q.E.D. for my ALL(a):[a≠0 =>
EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]. But it is clearly
beginner math. Isn't DC Proof a beginner tool? And isn't
set theory what beginners should learn?

Mostowski Collapse schrieb am Dienstag, 30. November 2021 um 20:52:42 UTC+1:
> My theorem doen't work with <=>:
> Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ
> It is still not poved by DC Proof.
> Dan Christensen schrieb am Donnerstag, 25. November 2021 um 17:31:45 UTC+1:
> > On Thursday, November 25, 2021 at 2:54:56 AM UTC-5, Mostowski Collapse wrote:
> > >... why didn't you prove:
> > >
> > > EXIST(z):ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] ?
> > >
> > I am not deriving every result of modern set theory. Just, as you requested that, "The image of a non-empty domain is non empty." The notion of the image of a domain of a function would seem to be a given.
> > > Too lazy to invoke your own DC Proof subset axiom?
> > >
> > You seem to be getting more desperate by the hour, Jan Burse. Maybe you should take a little offline vacation to ponder the worrisome direction your life has taken of late.
> >
> > Dan

Beginners should learn notions such as "surjective" and
"injective", how do you define these without set theory?

That ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a <=> f(x) e b] & b≠0]]
isn't provable has also to do with beginner notions.

Mostowski Collapse schrieb am Donnerstag, 2. Dezember 2021 um 01:34:50 UTC+1:
> Still struggling?
>
> You are confusing the axiom with what I want to prove.
> What I want to prove has no <=>. It has only =>.
> You know proofs start with axioms and then end with
> what one wants to prove. Then one can say Heureka, Q.E.D.
>
> There is still no Heureka, Q.E.D. for my ALL(a):[a≠0 =>
> EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]. But it is clearly
> beginner math. Isn't DC Proof a beginner tool? And isn't
> set theory what beginners should learn?
> Mostowski Collapse schrieb am Dienstag, 30. November 2021 um 20:52:42 UTC+1:
> > My theorem doen't work with <=>:
> > Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> > > Or formally, s≠0 stands for EXIST(c):[c e s]:
> > > ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> > https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ
> > It is still not poved by DC Proof.
> > Dan Christensen schrieb am Donnerstag, 25. November 2021 um 17:31:45 UTC+1:
> > > On Thursday, November 25, 2021 at 2:54:56 AM UTC-5, Mostowski Collapse wrote:
> > > >... why didn't you prove:
> > > >
> > > > EXIST(z):ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] ?
> > > >
> > > I am not deriving every result of modern set theory. Just, as you requested that, "The image of a non-empty domain is non empty." The notion of the image of a domain of a function would seem to be a given.
> > > > Too lazy to invoke your own DC Proof subset axiom?
> > > >
> > > You seem to be getting more desperate by the hour, Jan Burse. Maybe you should take a little offline vacation to ponder the worrisome direction your life has taken of late.
> > >
> > > Dan

On Wednesday, December 1, 2021 at 7:35:46 PM UTC-5, Mostowski Collapse wrote:
> Beginners should learn notions such as "surjective" and
> "injective", how do you define these without set theory? ....

See my replies just now to your identical posting at sci.logic

Dan

*****************************************************
Hello Dan-O-Matik, WAKE UP, see below at end of post
how x e a has switched sides, same for x e b?
*****************************************************

Dan Christensen schrieb am Donnerstag, 2. Dezember 2021 um 18:46:31 UTC+1:
> Perhaps, you didn't know, but every set is a superset of itself.
> And if A <=> B, then A => B. I hope this helps.

You are extremly crazy right now, just because you don't
read what is before your eyes. Can you show how you go from 1):

/* not provable */
1) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a <=> f(x) e b] & b≠0]]

To this here 2), when 1) isn't provable?

/* provable */
2) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]

You forget that 1) is not in the form of the axiom schema of replacement.
The exists quatifier is missing. To be in the form of the axiom schema of
replacement it would need to read:

/* provable */
3) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e b <=> EXIST(y):[y e a & f(y)=x]] & b≠0]]

How do you want to go from 3) to 2) by chaning <=> into =>.
You are crazy. What about the EXIST quantifier? Did you
also see that x e a has switched sides, same for x e b?

Dan Christensen schrieb am Donnerstag, 2. Dezember 2021 um 06:18:38 UTC+1:
> On Wednesday, December 1, 2021 at 7:35:46 PM UTC-5, Mostowski Collapse wrote:
> > Beginners should learn notions such as "surjective" and
> > "injective", how do you define these without set theory? ....
>
>
> See my replies just now to your identical posting at sci.logic
>
> Dan

You are correct in your "thinking" so informally something
happens going from codomain to superset of codomain.

But formally its not so simple going from A<=>B to A=>B,
because already the direction is somehow wrong.

Can you prove my formula in DC Proof, yes or no?

Mostowski Collapse schrieb am Donnerstag, 2. Dezember 2021 um 21:17:08 UTC+1:
> *****************************************************
> Hello Dan-O-Matik, WAKE UP, see below at end of post
> how x e a has switched sides, same for x e b?
> *****************************************************
>
> Dan Christensen schrieb am Donnerstag, 2. Dezember 2021 um 18:46:31 UTC+1:
> > Perhaps, you didn't know, but every set is a superset of itself.
> > And if A <=> B, then A => B. I hope this helps.
>
> You are extremly crazy right now, just because you don't
> read what is before your eyes. Can you show how you go from 1):
>
> /* not provable */
> 1) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a <=> f(x) e b] & b≠0]]
>
> To this here 2), when 1) isn't provable?
>
> /* provable */
> 2) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
>
> You forget that 1) is not in the form of the axiom schema of replacement.
> The exists quatifier is missing. To be in the form of the axiom schema of
> replacement it would need to read:
>
> /* provable */
> 3) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e b <=> EXIST(y):[y e a & f(y)=x]] & b≠0]]
>
> How do you want to go from 3) to 2) by chaning <=> into =>.
> You are crazy. What about the EXIST quantifier? Did you
> also see that x e a has switched sides, same for x e b?
> Dan Christensen schrieb am Donnerstag, 2. Dezember 2021 um 06:18:38 UTC+1:
> > On Wednesday, December 1, 2021 at 7:35:46 PM UTC-5, Mostowski Collapse wrote:
> > > Beginners should learn notions such as "surjective" and
> > > "injective", how do you define these without set theory? ....
> >
> >
> > See my replies just now to your identical posting at sci.logic
> >
> > Dan

So we have now two unresolved problems for DC proof:
1) Still no proof of ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
2) Still no correct definition of F : X -> Y

Here is my prediction what we will discuss X-mas:
3) Denial of 3 ⊆ 5 for von Neuman ordinals
4) The moon is made of cheese

LoL

Mostowski Collapse schrieb am Donnerstag, 2. Dezember 2021 um 21:27:59 UTC+1:
> You are correct in your "thinking" so informally something
> happens going from codomain to superset of codomain.
>
> But formally its not so simple going from A<=>B to A=>B,
> because already the direction is somehow wrong.
>
> Can you prove my formula in DC Proof, yes or no?
> Mostowski Collapse schrieb am Donnerstag, 2. Dezember 2021 um 21:17:08 UTC+1:
> > *****************************************************
> > Hello Dan-O-Matik, WAKE UP, see below at end of post
> > how x e a has switched sides, same for x e b?
> > *****************************************************
> >
> > Dan Christensen schrieb am Donnerstag, 2. Dezember 2021 um 18:46:31 UTC+1:
> > > Perhaps, you didn't know, but every set is a superset of itself.
> > > And if A <=> B, then A => B. I hope this helps.
> >
> > You are extremly crazy right now, just because you don't
> > read what is before your eyes. Can you show how you go from 1):
> >
> > /* not provable */
> > 1) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a <=> f(x) e b] & b≠0]]
> >
> > To this here 2), when 1) isn't provable?
> >
> > /* provable */
> > 2) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
> >
> > You forget that 1) is not in the form of the axiom schema of replacement.
> > The exists quatifier is missing. To be in the form of the axiom schema of
> > replacement it would need to read:
> >
> > /* provable */
> > 3) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e b <=> EXIST(y):[y e a & f(y)=x]] & b≠0]]
> >
> > How do you want to go from 3) to 2) by chaning <=> into =>.
> > You are crazy. What about the EXIST quantifier? Did you
> > also see that x e a has switched sides, same for x e b?
> > Dan Christensen schrieb am Donnerstag, 2. Dezember 2021 um 06:18:38 UTC+1:
> > > On Wednesday, December 1, 2021 at 7:35:46 PM UTC-5, Mostowski Collapse wrote:
> > > > Beginners should learn notions such as "surjective" and
> > > > "injective", how do you define these without set theory? ....
> > >
> > >
> > > See my replies just now to your identical posting at sci.logic
> > >
> > > Dan