Is my proof correct?
Notations:
$\mathbb{N}$:=$\{1,2,3,..
\}$ = The set of all natural numbers.
$J_q$:=$\{ y : 1\leq y \leq q, \text{ for some } q \in \mathbb{N}\}$ = The set of first $q$ natural numbers.
$|W|:=$ The cardinality of set $W$.
$ v:T \rightarrow U $ is read as '$v$ is a function from $T$ to $U$, where $T$ and $U$ are sets.'
Proof:
$$\begin{align}\text{Let }A \text{ and } B \text{ be any two finite sets. }\tag{1}\label{eq1}\end{align}$$
$$\begin{equation}\begin{aligned} \text{If } A=\varnothing \text{ and } B=\varnothing, \text{ then }A\cup B=\varnothing.\\ \text{If } A\neq\varnothing \text{ and } B=\varnothing, \text{ then }A\cup B=A.\\ \text{If } A=\varnothing \text{ and } B\neq\varnothing, \text{ then }A\cup B=B.\\ \text{If } A\neq\varnothing \text{ and } B\neq\varnothing \text{ such that } A=B, \text{ then }A\cup B=A=B.\\ \end{aligned}\end{equation}\tag{2}\label{eq2}$$
$$\begin{align}\text{Now, let } A\neq B \text{ and } |A|=n, \ |B|=m \\ \text{ for some } n,m \in \mathbb{N}\tag{3} \label{eq3}\end{align}$$
We know that $A \cup B = A \cup (B/A)$
Let $f:J_n \rightarrow A$ such that $f(i):=a_i, \forall i \in J_n \ \implies f $ is bijective.
Let $|B/A|=p$, for some $p \in \mathbb{N}$. Since, $B/A$ is a subset of $B$, we have $p\leq m$.
Let $g:(J_{n+p}\backslash J_n)\rightarrow (B/A)$ such that $g(n+j):=b_j, \forall j \in J_m$. $\implies g$ is bijective.
Let $h:J_{n+p}\rightarrow A \cup B $ such that
$$h(x):=\begin{cases}f(x), & \forall x \in J_n \\ g(n+x), & \forall x \in (J_{n+p}/J_n) \end{cases}$$
$$\because \ B/A \cap A = \varnothing \ \\ \implies f(\omega)\neq g(\lambda), \forall \omega \in J_n, \forall \lambda \in (J_{n+p}/J_n)$$
Let $\theta \in A \cup B$ $\implies \theta \in A$ or $\theta \in B/A$ $\implies \ \exists s \in \mathbb{N}, s\leq n \text{ such that }\theta=a_s$ or $\exists r \in \mathbb{N}, r\leq p \text{ such that }\theta=b_r$ $\implies \theta=f(s)=h(s)$ or $\theta=g(n+r)=h(r)$ $(\because f \text{ and } g \text{ are onto.})$
Thus, $h$ is onto $\implies |A\cup B|\leq |J_{n+p}|=n+p$ $$\begin{equation}\begin{aligned}\implies \text{If } A\neq\varnothing \text{ and } B\neq\varnothing \text{ such that } A\neq B, \text{ then } A\cup B \text{ is finite}\end{aligned}\end{equation}\tag{4}\label{eq4}$$
$(1),(2),(3),(4) \implies$ for any two finite sets, their union is always finte.
I think you are probably overcomplicating things with your approach. Don't worry about the overlap elements or if they are the same. You can eliminate the empty set as you do to keep needing to worry about empty bijections (Though it wouldn't pose a problem)
By definition of being nonempty/finite, you have a bijection $f:J_n\to A$ and $g:J_m\to B$ for some $n,m\in \mathbb{N}$. Define $h:J_{n+m}\to A\cup B$ as $h(i)=f(i)$ if $i\leq n$, otherwise $h(i)=g(i-n)$.
This is a surjection, so by the one axiom you are using, you have $|A\cup B|\leq |J_{n+m}|$, hence finite.