Rigorous proof that cardinality of a disjoint union is the sum of cardinalities for finite sets

Question

In a lot of books there are intuitive(but sort of hand wavy) proofs for finite, disjoint sets $A$ and $B$ that $$ |A \cup B| = |A| + |B| $$ since $A = \{a_1,a_2,a_3,\cdots,a_{|A|}\}$ and $B = \{b_1,b_2,b_3,\cdots,b_{|B|}\}$ are disjoint collections, and we can list them as $$ a_1,a_2,a_3,\cdots,a_{|A|},b_{|A| + 1},b_{|A| + 2},b_{|A| + 3},\cdots,b_{|A| + |B|}. $$ For a more rigorous proof, would we first prove $$ f: k \longmapsto m + k, \quad 1 \leq k \leq n $$ is a bijection to $\{m + 1,m + 2,m+3,\cdots,m+n\}$, and then show $1,2,3,\cdots,|A|$ and $|A| + 1, |A| + 2, |A| + 3,\cdots, |A| + |B|$ exhausts all naturals $1 \leq k \leq |A| + |B|$. I was somewhat amazed at how complicated Proof Wiki's version went and was wondering if we really needed all the machinery that they used.