You need to give us much more information on the axioms of set theory that you are using. What is the definition of finiteness in this set theory? How do these axioms force an order on the way you define and prove things?

@RobArthan excellent point, I shall add the axioms.

This remind me of the book Principia Mathematica. You are building things from scratch, amazing.

@seayellow I do have a copy of that book actually, perhaps such a thing is covered in there somewhere!

@Graviton I'd like to read it but it must be very tedious.

What is the formal definition of your set $Z$. Your axioms don't justify defining a set by giving an infinite list of its elements.

@RobArthan once again, good point, I shall instead replace it with the formal definition,

@seayellow: there is a rich literature on the foundations of mathematics. Russell and Whitehead were pioneers in this subject and their Principia Mathematica is a seminal work, but other systems, most notably Zermelo-Fraenkel set theory, have been more widely used and studied

@RobArthan Thanks for that! Really interesting.

Why not do the contrary? I mean, show that there is not an injective function from $A\cup B$ to $A$? What is your definition of function?

@yoyo I am similarly stuck on that approach too. My definition is the standard set theoretic approach where if $f$ is a function $f:X\to Y$ then $f\subseteq X\times Y$. Ordered pairs can be defined by Kuratowski pairs.

I'm not convinced your definition of $Z$ actually defines a set. Unless I'm missing something, in ZFC the property you give as a definition is satisfied by at least every $H_{\beth_\alpha}$ where $\alpha$ is a limit ordinal.

@Troposphere, forgive me, but what is $H$? I assume $\beth_\alpha$ is a beth number, in which case this is already probably far past my level of understanding. How is $Z$ not a set? What's the alternative?

@Graviton: Yes, $\beth_\alpha$ is a beth number -- in particular, when $\alpha$ is a limit ordinal, $\beth_\alpha$ has the property that $2^{\kappa} < \beth_\alpha$ for every $\kappa < \beth_\alpha$. Now $H_{\beth_\alpha}$ is the set of all sets that hereditarily have cardinality less than $\beth_\alpha$ -- that is: a set is an element of $H_{\beth_\alpha}$ iff it and its element and its elements' elements, and so forth, all have cardinality less than $\beth_\alpha$.

Do you have that the union over the element of the set of singletons of $A$ is $A$ itself?

So the problem is not that $Z$ might not be a set, but that it's very possible that a model of your axioms contain many different sets that each satisfy your definition for $Z$ (and most of them contain elements that we would ordinarily count as "infinite"). Since your definition doesn't single out a particular one of them, it doesn't actually define a set.

@yoyo I'm not sure if I quite follow, are you asking if $\cup\{A\}=A$ or $\bigcup_{a\in A}\{a\}=A$ or...?

And if someone nevertheless gives you a particular $Z$ that satisfies the definition, then the claim you eventually want to prove might not actually true for the concept of "fininte" that arises from comparing to that $Z$ -- after all, the $Z$ you got might be $H_{\beth_\omega}$, and $|H_{\beth_\omega}|=\beth_\omega \ggg |\mathbb N|$.

@Graviton: I seem to be failing to make my point understandably here -- the trouble in this case isn't "some definitions not actually sets", but instead "some definitions not actually definitions". When we say "define $X$ by: $X$ has such and such property", that only works as a definition if we can prove that there is a thing but only one thing that has the property. The "only one" part fails for your property for $Z$.

@Troposphere, ahh, I see. And this is still a problem despite the existential quantifier being "there exists", rather than "there exists exactly one", because there isn't one such set $Z$ that has such property?

Well, with a quantifier you just have a claim, which has a truth value (i.e. it can be true or false that there are sets with that property), but it doesn't define anything.

What you may want to do is to define a new set to be the intersection of all the $Z$s that satisify the given property. This is meaningful if you have an axiom that says at least one $Z$ exists. Then you can (with some effort) prove that $\bigcap\{\text{all }Z\text{s}\}$ also itself satisfies the property, and it turns out it is the set of all heriditarily finite sets, called $H_{\aleph_0}$ or $V_{\omega}$, which is countable. You can then use this set to represent $\mathbb N$ using Ackermann's representation.

Or perhaps $|x|\ne |Z|$ in your property for $Z$ should have been $|x|\le 1$? In that case it would be provable (using Regularity) that there's only one $Z$ that satisfies it.

@Troposphere, ah yes, that is clever. Cheers for the update. I shall meditate on this.

@Troposphere Your argument that the property holds for $H_{\beth_\omega}$ appears not to work, because it appears to require that $\beth_\omega$ is a regular cardinal (hence a weakly inaccessible cardinal). How did you show that $|H_{\beth_\omega}| = \beth_\omega$ without assuming that $\beth_\omega$ is regular?