By definition of cardinality, $|X|=|Y|$ if there exists a bijective function $f:X\to Y$.
I would like to rigorously prove that if $A$ is a finite set, then $|A|\neq |A\cup B|$ when $B\not\subseteq A$. However, this seems less trivial than anticipated.
I must point out, the reason this is less trivial than anticipated is that I am working in a set theory in which I have to prove this before I define the natural numbers. In other words, I cannot simply claim that since $A$ is finite, there exists a bijection between it and some set $\{0,\dots,n\}$, or claim that $A=\{a_1,\dots,a_n\}$ (as is done in the answer to this question) where $n\in\mathbb{N_0}$, because the natural numbers are not defined yet. So, by finite, what I mean is that at the very least, we know that $|A|<|Z|$, where the countably infinite set $Z$ is defined by
$$\exists Z[\emptyset,\{\emptyset\}\in Z\wedge\forall x(x\in Z \iff x\subseteq Z\wedge |x|\neq |Z|)]$$
It seems natural to start with a proof by contradiction. So, on the contrary, let's suppose $|A|=|A\cup B|$. Thus, there must exist some bijective function $g:A\to A\cup B$. This is where I immediately find myself stuck. To you and I, this is a trivial impossibility, as the range of $g$ is bigger than the domain. Hence, there must exist some $b\in A\cup B$ s.t. $\nexists a\in A(g(a)=b).$
However, this does not seem rigorous to me. It seems I have just jumped to the conclusion and claimed that there is a contradiction in plain language because I am biased by knowing that it was true in the first place. I would like to know how to formulate this proof more concretely.
How do I prove this with as few logical leaps as possible, without reference to the natural numbers, and hopefully pertaining as closely as I can to first-order logic alone?
Edit: As pointed out in the comments, I should specify what axioms can be assumed.
Axioms: We can assume many of the axioms of ZF, such as Extensionality, Regularity, Specification, Pairing, Union, and Powerset.
Sets: We can also assume that the empty set, $\emptyset$, exists, that the previously mentioned $Z$ exists, and that $A\in Z$ (hence why it must be the case that $|A|<|Z|$ since $A\in Z \implies A\subseteq Z\wedge |A|\neq|Z|$). Importantly, we can also assume that all sets are hereditary sets.
Cardinality: On top of the definition for cardinality equality, we can assume that $|X|\leq|Y|$ if there exists an injective function from $X$ into $Y$. Let's say that $X$ is finite if it has cardinality equal to the cardinality of some subset of $Z$, but cardinality not equal to $|Z|$.
Suppose there is some bijection $g : A \cup B \to A$.
Take $b \in B$ such that $b \notin A$. Consider the sequence $s : Z \to A \cup B$ defined by $s_0 = b$ and $s_{succ(n)} = g(s_n)$.
Claim: $s: Z \to A \cup B$ is injective.
Proof: We must show for all $n \in Z$, for all $m \in Z$, $s_n = s_m$ implies $n = m$. We proceed by induction on $n$.
Case 1: $n = 0$. we must show that for all $m \in Z$, $s_m = b$ implies $m = 0$. We proceed by induction on $m$.
Case 1a: $m = 0$. Immediate. Case 1b: $m = succ(k)$. Then $b = s_{succ(k)} = g(s_k)$. Now $g(s_k) \in A$, but $b \notin A$. Contradiction.
Case 2: $n = succ(k)$ and for all $m$, if $s_m = s_k$ then $m = k$. We must show for all $m \in Z$, if $s_m = g(s_k)$ then $m = succ(k)$. We proceed by induction on $m$.
Case 2a: $m = 0$. Then $b = g(s_k)$. Again, this cannot happen. Case 2b: $m = succ(j)$. Then $g(s_j) = g(s_k)$. Then $s_j = s_k$. Then $j = k$. Then $m = succ(k)$.
Thus, we see that $|Z| \leq |A \cup B| = |A|$.
But you have already stated by assumption that $|A| < |Z|$. Contradiction.
Note: you might need Cantor-Schroder-Bernstein for the last bit. But the proof of that is fairly elementary.
Edit: my answer was meant to work with OP's original definition of $Z$ as $\{\emptyset, \{\emptyset\}, \{\{\emptyset\}\}, ..., \}$. However, OP has since attempted to redefine $Z$.
The problem, as @Troposphere has pointed out, is that OP's attempted definition of $Z$ may not necessarily uniquely define $Z$.
I am not certain that this is actually the case, since @Troposphere's argument appears to rely on claim that $\beth_\omega$ is a regular cardinal. So I will further update this post when I have a good idea whether this is true.
Edit 2: If there is a strongly inaccessible cardinal $\lambda$, then $V_\lambda$ satisfies the condition for $Z$. I do not know if any uncountable set satisfying the condition for $Z$ must be an inaccessible cardinal, but I have shown that any such cardinal must be regular (which precludes @Troposphere's attempt).
So this definition of $Z$ doesn't work (unless ZF proves there are no strongly inaccessible cardinals, which seems unlikely).
Why does $|Z|$ have to be regular? Let $\alpha = |Z|$.
Note that for all $a, b \in Z$, we have $\{a, b\} \subseteq Z$ and $|\{a, b\}| \leq 2 < |Z|$ (since $\emptyset, \{\emptyset\}, \{\{\emptyset\}\} \in Z$). Therefore, $\{a, b\} \in Z$.
Thus, if $a, b \in Z$, we have $\{a\} = \{a, a\} \in Z$ and $\{a, b\} \in Z$. Therefore, $(a, b) = \{\{a\}, \{a, b\}\} \in Z$.
Consider the fact that for all ordinals $\beta < \alpha$, we have $\beta \in Z$. This can be proved by ordinal induction, since if $\beta < \alpha$ and for all $\gamma \in \beta$, $\gamma \in Z$, then we have $|\beta| < Z$ and $\beta \subseteq Z$; hence, $\beta \in Z$.
Now suppose $\beta < \alpha$ is an ordinal. Consider the fact that a function $f : \beta \to Z$ is a set of cardinality $|\beta| < \alpha$, and consider that each element of $f$ is a pair $(\gamma, z)$, where $z \in Z$ and $\gamma \in \beta \in Z$. Therefore, each $f : \beta \to Z$ is an element of $Z$. So $Z^\beta \subseteq Z$ for all $\beta < \alpha$.
Consider some $\beta < \alpha$ and some ordinals $C_\gamma < \alpha$ for $\gamma < \beta$. Let $\lambda = \sup\limits_{\gamma \in \beta} C_\gamma < \alpha$. I claim that $\lambda < \alpha$.
For consider functions $\lambda \to Z$. Let us define $f : (\lambda \to Z) \to Z$ as follows:
For each $g : \lambda \to Z$, for each $\gamma \in \beta$, we define $f_g(\gamma) = g|_{C_\gamma} : C_\gamma \to Z$. Since we know that $(C_\gamma \to Z) \subseteq Z$, we see that $f_g(\gamma) \in Z$ for all $\gamma$. Hence, $f_g : \beta \to Z$, so $f_g \in Z$ for all $g$.
And we can recover $g$ from $f_g$, since $\bigcup\limits_{\gamma \in \beta} C_\gamma = \lambda$ and we can recover any function from its restriction to a covering. Therefore, $f$ is injective. Then we see that $\lambda < 2^\lambda \leq |Z^\lambda| \leq |Z| = \alpha$. So $\lambda < \alpha$, as required.
Therefore, $\alpha$ must be a regular cardinal.
I do not see how to extend this to a proof that $|Z|$ must be a strong limit cardinal. But I suspect that is the case.