It prevents EXISTUNIQUE because you can find (f1,c1)
and (f2, c2), where f1≠f2 and:

ALL(b):[b in c1 => f1(b)=b]]

ALL(b):[b in c2 => f2(b)=b]]

Now if you futher have constructed (f1,c1) and (f2,c2)
such that a ⊆ c1 and a ⊆ c2, then you can downgrade
the two and you get:

ALL(b):[b in a => f1(b)=b]]

ALL(b):[b in a => f2(b)=b]]

And this breaks EXISTUNIQUE. Its really extremly trivial.
Just use the Downgrade Lemma.

Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 20:49:03 UTC+1:
> The deeper problem is not Terrence Tao versus Dan-O-Matik
> versus metamath. In all 3 approaches this here then fails:
>
> /* Not Provable */
> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
>
> Thats very easy to see. Just chew on the downgrade Lemma:
>
> /* Downgrade Lemma */
> ALL(b):[b in a => b in c] & ALL(b):[b in c => f(b)=b]] => ALL(b):[b in a => f(b)=b]]
>
> The tree tool of Wolfgang Schwartz can prove it, you
> can also prove it with DC Proof, can't you:
>
> /* Encoding E__ stands for _ in _ */
> ∀x(Exa → Exc), ∀x(Exc → f(x)=x) entails ∀x(Exa → f(x)=x).
> https://www.umsu.de/trees/#~6x%28Exa~5Exb%29,~6x%28Exb~5f%28x%29=x%29|=~6x%28Exa~5f%28x%29=x%29
>
> Do you know what it says?
> Do you know why it prevents EXISTUNIQUE?

On Tuesday, December 14, 2021 at 2:49:03 PM UTC-5, Mostowski Collapse wrote:
> The deeper problem is not Terrence Tao versus Dan-O-Matik
> versus metamath. In all 3 approaches this here then fails:
>

You fail, Jan Burse, because you do not understand that f(x) is meaningless (undefined) if x is outside the domain of function f. You have painted yourself into this corner and now look like an idiot claiming the functions so defined are not unique. They are unique. Deal with it.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

By all means, you cannot prove this here:

/* Not Provable */
ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]

This is impossible. Prove me wrong. Prove it.

Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 21:33:10 UTC+1:
> On Tuesday, December 14, 2021 at 2:49:03 PM UTC-5, Mostowski Collapse wrote:
> > The deeper problem is not Terrence Tao versus Dan-O-Matik
> > versus metamath. In all 3 approaches this here then fails:
> >
> You fail, Jan Burse, because you do not understand that f(x) is meaningless (undefined) if x is outside the domain of function f. You have painted yourself into this corner and now look like an idiot claiming the functions so defined are not unique. They are unique. Deal with it.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

BTW: This is also not provable:

/* Not Provable */
ALL(a):[Set(a) => EXISTUNIQUE(f):[Set'(f) & ALL(b):[b in a => (b,b) in f]]]

Maybe easier to first digest that this is not provable.

Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 21:53:36 UTC+1:
> By all means, you cannot prove this here:
> /* Not Provable */
> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> This is impossible. Prove me wrong. Prove it.
> Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 21:33:10 UTC+1:
> > On Tuesday, December 14, 2021 at 2:49:03 PM UTC-5, Mostowski Collapse wrote:
> > > The deeper problem is not Terrence Tao versus Dan-O-Matik
> > > versus metamath. In all 3 approaches this here then fails:
> > >
> > You fail, Jan Burse, because you do not understand that f(x) is meaningless (undefined) if x is outside the domain of function f. You have painted yourself into this corner and now look like an idiot claiming the functions so defined are not unique. They are unique. Deal with it.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, December 14, 2021 at 3:53:36 PM UTC-5, Mostowski Collapse wrote:
> By all means, you cannot prove this here:
> /* Not Provable */
> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> This is impossible. Prove me wrong. Prove it.

Still in denial, I see. Really kind of pathetic.

I have posted the proof twice in this thread. Deal with it, Jan Burse.

Dan

No denial, you didn't post a proof, where you use EXISTUNIQUE(f).
You used your custom EXISTUNIQUE(f,a), which has a domain
parameter a. But the question is whether this here is provable or not:

On Tuesday, December 14, 2021 at 3:53:36 PM UTC-5, Mostowski Collapse wrote:
> By all means, you cannot prove this here:
> /* Not Provable */
> ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> This is impossible. Prove me wrong. Prove it.

Maybe you are a little confused?

Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 22:35:27 UTC+1:
> On Tuesday, December 14, 2021 at 3:53:36 PM UTC-5, Mostowski Collapse wrote:
> > By all means, you cannot prove this here:
> > /* Not Provable */
> > ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> > This is impossible. Prove me wrong. Prove it.
> Still in denial, I see. Really kind of pathetic.
>
> I have posted the proof twice in this thread. Deal with it, Jan Burse.
>
> Dan

You used this EXISTUNIQUE(f,a):

EXISTUNIQUE(f,a):A(f) <=> EXIST(h):[A(h) & ALL(f):ALL(g):[A(f) & A(g) => f|a = g|a]]

But my claim is you cannot prove it with EXISTUNIQUE(f):

EXISTUNIQUE(f):A(f) <=> EXIST(h):[A(h) & ALL(f):ALL(g):[A(f) & A(g) => f = g]]

I made this pretty clear here, when I wrote:
"You didn't prove f=g"

Whats wrong with you?

Mostowski Collapse schrieb am Dienstag, 14. Dezember 2021 um 22:39:00 UTC+1:
> No denial, you didn't post a proof, where you use EXISTUNIQUE(f).
> You used your custom EXISTUNIQUE(f,a), which has a domain
> parameter a. But the question is whether this here is provable or not:
>
> On Tuesday, December 14, 2021 at 3:53:36 PM UTC-5, Mostowski Collapse wrote:
> > By all means, you cannot prove this here:
> > /* Not Provable */
> > ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> > This is impossible. Prove me wrong. Prove it.
>
> Maybe you are a little confused?
> Dan Christensen schrieb am Dienstag, 14. Dezember 2021 um 22:35:27 UTC+1:
> > On Tuesday, December 14, 2021 at 3:53:36 PM UTC-5, Mostowski Collapse wrote:
> > > By all means, you cannot prove this here:
> > > /* Not Provable */
> > > ALL(a):[Set(a) => EXISTUNIQUE(f):ALL(b):[b in a => f(b)=b]]
> > > This is impossible. Prove me wrong. Prove it.
> > Still in denial, I see. Really kind of pathetic.
> >
> > I have posted the proof twice in this thread. Deal with it, Jan Burse.
> >
> > Dan

I dont think DC proof correctly associates functions and function graphs.
You can also try Terence Tao decrement example:

Example 3.3.2:
Unfortunately this does not define a function, because
when x = 0 there is no natural number y whose increment
is equal to x (Axiom 2.3). On the other hand, we can legitimately
define a decrement function h : N\{0} → N associated to
the property P(x,y) defined by y++ = x.
https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf

I think its is provable:

~EXIST(y):P(0,y)

Or do you claim otherwise?
Do you also have dark booleans for decrement?

LMAO!

Or asked differently how many decrement functions are
there in Peano arithmetic? Can you prove:

EXISTUNIQUE(h):"h is the decrement function"

Mostowski Collapse schrieb am Samstag, 18. Dezember 2021 um 14:20:59 UTC+1:
> I dont think DC proof correctly associates functions and function graphs.
> You can also try Terence Tao decrement example:
>
> Example 3.3.2:
> Unfortunately this does not define a function, because
> when x = 0 there is no natural number y whose increment
> is equal to x (Axiom 2.3). On the other hand, we can legitimately
> define a decrement function h : N\{0} → N associated to
> the property P(x,y) defined by y++ = x.
> https://lms.umb.sk/pluginfile.php/111477/mod_page/content/5/TerenceTao_Analysis.I.Third.Edition.pdf
>
> I think its is provable:
>
> ~EXIST(y):P(0,y)
>
> Or do you claim otherwise?
> Do you also have dark booleans for decrement?
>
> LMAO!

On Tuesday, December 14, 2021 at 4:39:00 PM UTC-5, Mostowski Collapse wrote:
> No denial, you didn't post a proof, where you use EXISTUNIQUE(f).
> You used your custom EXISTUNIQUE(f,a), which has a domain
> parameter a. But the question is whether this here is provable or not:

Still in denial, I see. I have twice posted proof of the uniqueness of the identity function on any given set, i.e. the same input will result in the same output. Deal with it, Jan Burse. You are looking like a complete idiot here, in the same league as AP, JG and WM. If you are simply going to keep repeating your absurd claims as here, do not expect a reply from me on this matter.

Dan

The harder I look the less your nonsense makes any sense. Those
people calling other people cranks, are often cranks themselves.

Can you show us the decrement function in DC Proof. If
I take your approach and only define it as:

ALL(a):[a in N \ {0} => h(a)++ = a]

I can still prove in DC Proof:

EXIST(b):h(0)=b

But Terrence Tao says "decrement function h : N\{0} → N
associated to the property P(x,y) defined by y++ = x".

Dan Christensen schrieb am Samstag, 18. Dezember 2021 um 15:07:46 UTC+1:
> On Tuesday, December 14, 2021 at 4:39:00 PM UTC-5, Mostowski Collapse wrote:
> > No denial, you didn't post a proof, where you use EXISTUNIQUE(f).
> > You used your custom EXISTUNIQUE(f,a), which has a domain
> > parameter a. But the question is whether this here is provable or not:
> Still in denial, I see. I have twice posted proof of the uniqueness of the identity function on any given set, i.e. the same input will result in the same output. Deal with it, Jan Burse. You are looking like a complete idiot here, in the same league as AP, JG and WM. If you are simply going to keep repeating your absurd claims as here, do not expect a reply from me on this matter.
>
> Dan

Now take Terence Taos definition of f=g. He says
f=g for f, g: X->Y: f=g iff forall x(x e X => f(x)=g(x)).

Now take f, g: N -> N with:

f(x)=if x=\=0 then x-1 else 3
g(x)=if x=\=0 then x-1 else 4

Both satisfy a Dan-O-Matik definition:

ALL(a):[a in N \ {0} => f(a)++ = a]
ALL(a):[a in N \ {0} => g(a)++ = a]

But according to Terence Tao we have f=\=g.
So Dan-O-Matik has a hell of a lot of decrement functions.

LoL

Mostowski Collapse schrieb am Samstag, 18. Dezember 2021 um 15:36:18 UTC+1:
> The harder I look the less your nonsense makes any sense. Those
> people calling other people cranks, are often cranks themselves.
>
> Can you show us the decrement function in DC Proof. If
> I take your approach and only define it as:
>
> ALL(a):[a in N \ {0} => h(a)++ = a]
>
> I can still prove in DC Proof:
>
> EXIST(b):h(0)=b
>
> But Terrence Tao says "decrement function h : N\{0} → N
> associated to the property P(x,y) defined by y++ = x".
> Dan Christensen schrieb am Samstag, 18. Dezember 2021 um 15:07:46 UTC+1:
> > On Tuesday, December 14, 2021 at 4:39:00 PM UTC-5, Mostowski Collapse wrote:
> > > No denial, you didn't post a proof, where you use EXISTUNIQUE(f).
> > > You used your custom EXISTUNIQUE(f,a), which has a domain
> > > parameter a. But the question is whether this here is provable or not:
> > Still in denial, I see. I have twice posted proof of the uniqueness of the identity function on any given set, i.e. the same input will result in the same output. Deal with it, Jan Burse. You are looking like a complete idiot here, in the same league as AP, JG and WM. If you are simply going to keep repeating your absurd claims as here, do not expect a reply from me on this matter.
> >
> > Dan

What is easier to use, DC proof or ZFC? DC proof
claims that certain things are given:

> ALL(a):[a in D => f(a) in C] where D and C are the given domain and
> codomain sets. In this case, "f(x)" is undefined and quite meaningless for x not in D.

Is this true when we talk about functions? The domains
and co-domains cannot always be given so easily. Thats the
Dan-O-Matik paradox. For example there is this theorem:

"Every injective function f has an inverse function g on its range"

If f: A -> B, whats the domain of g? What does need less
steps to prove the above, DC proof or ZFC?

With ZFC I only need to do the following:

1) let g = { (y, x) | (x, y) in f}, show it is a set

2) show g is a function when f is injective

3) conclude dom(g) = ran(f)

I am pretty sure DC proof needs much more work. Since to
start with ALL(a):[a in A => f(a) in B] and end with existence
of g, D and C such that ALL(a):[a in D => g(a) in C],

it will anyway first construct g in the form of a set and then
use its function axiom. So its kind of set theory with extra
steps. Utter unnecessary nonsense to be precise.

Mostowski Collapse schrieb am Freitag, 24. Dezember 2021 um 10:24:14 UTC+1:
> What is easier to use, DC proof or ZFC? DC proof
> claims that certain things are given:
>
> > ALL(a):[a in D => f(a) in C] where D and C are the given domain and
> > codomain sets. In this case, "f(x)" is undefined and quite meaningless for x not in D.
>
> Is this true when we talk about functions? The domains
> and co-domains cannot always be given so easily. Thats the
> Dan-O-Matik paradox. For example there is this theorem:
>
> "Every injective function f has an inverse function g on its range"
>
> If f: A -> B, whats the domain of g? What does need less
> steps to prove the above, DC proof or ZFC?

On Friday, December 24, 2021 at 4:24:14 AM UTC-5, Mostowski Collapse wrote:
> What is easier to use, DC proof or ZFC? DC proof
> claims that certain things are given:
>
> > ALL(a):[a in D => f(a) in C] where D and C are the given domain and
> > codomain sets. In this case, "f(x)" is undefined and quite meaningless for x not in D.
>
> Is this true when we talk about functions? The domains
> and co-domains cannot always be given so easily. ...

When you want to introduce an arbitrary function in a proof, you should, at the very least, attach a name to the function, domain and codomain.

Example in DC Proof notation

1. Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
(Premise)

Where f is an arbitrary function on arbitrary sets x and y.

Then f(z) will be undefined (i.e. meaningless) if z is not in the domain set x. This is the usual practice in math textbooks. Quit pretending otherwise, Jan Burse.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

You are changing topic. I dont mind if you need Set(_)
as well in DC poop. The question is rather can you
prove this textbook theorem, i. e. EXIST(g) :

"Every injective function f has an inverse function g on its range"

But I guess you already gave up. A few weeks ago you
boasted ZFC or set theory is not found in everyday math.
What about the above theorem, what is needed in DC poop?

Dan Christensen schrieb am Freitag, 24. Dezember 2021 um 16:44:49 UTC+1:
> On Friday, December 24, 2021 at 4:24:14 AM UTC-5, Mostowski Collapse wrote:
> > What is easier to use, DC proof or ZFC? DC proof
> > claims that certain things are given:
> >
> > > ALL(a):[a in D => f(a) in C] where D and C are the given domain and
> > > codomain sets. In this case, "f(x)" is undefined and quite meaningless for x not in D.
> >
> > Is this true when we talk about functions? The domains
> > and co-domains cannot always be given so easily. ...
>
> When you want to introduce an arbitrary function in a proof, you should, at the very least, attach a name to the function, domain and codomain.
>
> Example in DC Proof notation
>
> 1. Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
> (Premise)
>
> Where f is an arbitrary function on arbitrary sets x and y.
>
> Then f(z) will be undefined (i.e. meaningless) if z is not in the domain set x. This is the usual practice in math textbooks. Quit pretending otherwise, Jan Burse.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Friday, December 24, 2021 at 5:49:24 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Freitag, 24. Dezember 2021 um 16:44:49 UTC+1:
> > On Friday, December 24, 2021 at 4:24:14 AM UTC-5, Mostowski Collapse wrote:
> > > What is easier to use, DC proof or ZFC? DC proof
> > > claims that certain things are given:
> > >
> > > > ALL(a):[a in D => f(a) in C] where D and C are the given domain and
> > > > codomain sets. In this case, "f(x)" is undefined and quite meaningless for x not in D.
> > >
> > > Is this true when we talk about functions? The domains
> > > and co-domains cannot always be given so easily. ...
> >
> > When you want to introduce an arbitrary function in a proof, you should, at the very least, attach a name to the function, domain and codomain.
> >
> > Example in DC Proof notation
> >
> > 1. Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
> > (Premise)
> >
> > Where f is an arbitrary function on arbitrary sets x and y.
> >
> > Then f(z) will be undefined (i.e. meaningless) if z is not in the domain set x. This is the usual practice in math textbooks. Quit pretending otherwise, Jan Burse.

> You are changing topic.

The topic was your bizarre notion of functions outside of their domain of definition, Jan Burse. Just admit you were wrong.

> I dont mind if you need Set(_)
> as well in DC poop. The question is rather can you
> prove this textbook theorem, i. e. EXIST(g) :
> "Every injective function f has an inverse function g on its range"

Trying to change the subject, Jan Burse? In any case, you might have a look at my formal proof of the Cantor-Burnstein-Schroeder theorem at http://dcproof.com/CBS.htm

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

So you cannot show existence of g?

Hiding behind some absurd claims the encoding
of functions as set of pairs is bizzar?

How do you show existence of g = f^-1 in DC proof?

LoL

On Sunday, December 26, 2021 at 5:04:17 AM UTC-5, Mostowski Collapse wrote:
> So you cannot show existence of g?
>

See the proof of "Existence of Inverse Function Lemma" at the above link. It proves the existence of the inverse of a bijection.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

It only proves:

"If a function is surjective and injection, then it has an inverse."
http://dcproof.com/ExistenceOfInverse.htm

The theorem that was demanded was:
"Every injective function f has an inverse function g on its range"

Dan Christensen schrieb am Sonntag, 26. Dezember 2021 um 16:23:12 UTC+1:
> On Sunday, December 26, 2021 at 5:04:17 AM UTC-5, Mostowski Collapse wrote:
> > So you cannot show existence of g?
> >
> See the proof of "Existence of Inverse Function Lemma" at the above link. It proves the existence of the inverse of a bijection.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Can you prove your ExistenceOfInverse without
using bizzar sets, like this here:

Define: f' (as subset of yx)
17 Set'(f')
Split, 16
18 ALL(a):ALL(b):[(a,b) e f' <=> (a,b) e yx & f(b)=a]

Or do you admit that you were loosing your head,
accusing other people of bizzar ideas, whereas
your DC poop cannot do without just these bizzar

ideas. I guess everybody will agree that

ALL(a) : ALL(b) : [~(a, b) e yx => ~(a, b) e f']

Maybe you stole the proof somewhere? And you are
cheater? How can you not know that you yourself
use bizzar concepts in DC poop?

Mostowski Collapse schrieb am Sonntag, 26. Dezember 2021 um 17:58:04 UTC+1:
> It only proves:
>
> "If a function is surjective and injection, then it has an inverse."
> http://dcproof.com/ExistenceOfInverse.htm
>
> The theorem that was demanded was:
> "Every injective function f has an inverse function g on its range"
> Dan Christensen schrieb am Sonntag, 26. Dezember 2021 um 16:23:12 UTC+1:
> > On Sunday, December 26, 2021 at 5:04:17 AM UTC-5, Mostowski Collapse wrote:
> > > So you cannot show existence of g?
> > >
> > See the proof of "Existence of Inverse Function Lemma" at the above link. It proves the existence of the inverse of a bijection.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Sunday, December 26, 2021 at 10:23:12 AM UTC-5, Dan Christensen wrote:
> On Sunday, December 26, 2021 at 5:04:17 AM UTC-5, Mostowski Collapse wrote:
> > So you cannot show existence of g?
> >
> See the proof of "Existence of Inverse Function Lemma" at the above link. It proves the existence of the inverse of a bijection.

Just now completed a proof (139 lines) of:

ALL(x):ALL(y):ALL(f):[Set(x)
& Set(y)
& EXIST(c):c in x
& ALL(c):[c in x => f(c) in y]
& ALL(c):ALL(d):[c in x & d in x => [f(c)=f(d) => c=d]]

=> EXIST(rf):EXIST(g):[Set(rf) & ALL(b):[b in rf <=> b in y & EXIST(c):[c in x & f(c)=b]]
& ALL(a):[a in rf => g(a) in x]
& ALL(a):[a in rf => f(g(a))=a]
& ALL(a):[a in rf => f(g(a))=a]]]

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

On Sunday, December 26, 2021 at 10:23:12 AM UTC-5, Dan Christensen wrote:
> On Sunday, December 26, 2021 at 5:04:17 AM UTC-5, Mostowski Collapse wrote:
> > So you cannot show existence of g?
> >
> See the proof of "Existence of Inverse Function Lemma" at the above link. It proves the existence of the inverse of a bijection.
> Dan
>

Just now completed a proof (139 lines) of:

ALL(x):ALL(y):ALL(f):[Set(x)
& Set(y)
& ALL(c):[c in x => f(c) in y]
& ALL(c):ALL(d):[c in x & d in x => [f(c)=f(d) => c=d]]

=> EXIST(rf):EXIST(g):[Set(rf) & ALL(b):[b in rf <=> b in y & EXIST(c):[c in x & f(c)=b]]
& ALL(a):[a in rf => g(a) in x]
& ALL(a):[a in rf => f(g(a))=a]
& ALL(a):[a in rf => f(g(a))=a]]]

> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Sunday, December 26, 2021 at 10:23:12 AM UTC-5, Dan Christensen wrote:
> On Sunday, December 26, 2021 at 5:04:17 AM UTC-5, Mostowski Collapse wrote:
> > So you cannot show existence of g?
> >
> See the proof of "Existence of Inverse Function Lemma" at the above link. It proves the existence of the inverse of a bijection.
> Dan
>

Just now completed a proof (138 lines) of the following:

ALL(x):ALL(y):ALL(f):[Set(x)
& Set(y)
& ALL(c):[c in x => f(c) in y]
& ALL(c):ALL(d):[c in x & d in x => [f(c)=f(d) => c=d]]

=> EXIST(rf):EXIST(g):[Set(rf) & ALL(b):[b in rf <=> b in y & EXIST(c):[c in x & f(c)=b]]
& ALL(a):[a in rf => g(a) in x]
& ALL(a):[a in rf => f(g(a))=a]]]

> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Why don't you show the proof?
Does it use bizzarro set theory?

Dan Christensen schrieb am Sonntag, 26. Dezember 2021 um 22:09:01 UTC+1:
> On Sunday, December 26, 2021 at 10:23:12 AM UTC-5, Dan Christensen wrote:
> > On Sunday, December 26, 2021 at 5:04:17 AM UTC-5, Mostowski Collapse wrote:
> > > So you cannot show existence of g?
> > >
> > See the proof of "Existence of Inverse Function Lemma" at the above link. It proves the existence of the inverse of a bijection.
> > Dan
> >
> Just now completed a proof (138 lines) of the following:
>
> ALL(x):ALL(y):ALL(f):[Set(x)
> & Set(y)
> & ALL(c):[c in x => f(c) in y]
> & ALL(c):ALL(d):[c in x & d in x => [f(c)=f(d) => c=d]]
>
> => EXIST(rf):EXIST(g):[Set(rf) & ALL(b):[b in rf <=> b in y & EXIST(c):[c in x & f(c)=b]]
> & ALL(a):[a in rf => g(a) in x]
> & ALL(a):[a in rf => f(g(a))=a]]]
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com