[proofplan]
Choose bijections $f:A\to A'$ and $g:B\to B'$. We construct three induced maps: one on tagged disjoint unions, one on Cartesian products, and one on function sets. In each case the inverse is obtained by replacing $f$ and $g$ with their inverse bijections, so each induced map is a bijection and therefore preserves cardinality.
[/proofplan]
[step:Choose bijections witnessing the two cardinal equalities]
Since $|A|=|A'|$, choose a bijection
\begin{align*}
f:A&\to A'.
\end{align*}
Since $|B|=|B'|$, choose a bijection
\begin{align*}
g:B&\to B'.
\end{align*}
Let
\begin{align*}
f^{-1}:A'&\to A,\\
g^{-1}:B'&\to B
\end{align*}
denote their inverse maps.
[/step]
[step:Build a bijection between the disjoint unions]
We regard $A\sqcup B$ as the tagged union $(A\times\{0\})\cup(B\times\{1\})$, and similarly $A'\sqcup B'=(A'\times\{0\})\cup(B'\times\{1\})$. Define
\begin{align*}
F:A\sqcup B&\to A'\sqcup B'\\
(a,0)&\mapsto (f(a),0)\\
(b,1)&\mapsto (g(b),1).
\end{align*}
Define also
\begin{align*}
F^{-}:A'\sqcup B'&\to A\sqcup B\\
(a',0)&\mapsto (f^{-1}(a'),0)\\
(b',1)&\mapsto (g^{-1}(b'),1).
\end{align*}
For every $(a,0)\in A\times\{0\}$,
\begin{align*}
F^{-}(F(a,0))=F^{-}(f(a),0)=(f^{-1}(f(a)),0)=(a,0),
\end{align*}
and for every $(b,1)\in B\times\{1\}$,
\begin{align*}
F^{-}(F(b,1))=F^{-}(g(b),1)=(g^{-1}(g(b)),1)=(b,1).
\end{align*}
Thus $F^{-}\circ F=\operatorname{id}_{A\sqcup B}$. The same computation using $f(f^{-1}(a'))=a'$ and $g(g^{-1}(b'))=b'$ gives $F\circ F^{-}=\operatorname{id}_{A'\sqcup B'}$. Hence $F$ is a bijection, so $|A\sqcup B|=|A'\sqcup B'|$.
[guided]
The disjoint union remembers which summand an element came from. We implement this by tags: elements of $A\sqcup B$ are either $(a,0)$ with $a\in A$ or $(b,1)$ with $b\in B$. The natural map sends the $A$-summand through $f$ and the $B$-summand through $g$:
\begin{align*}
F:A\sqcup B&\to A'\sqcup B'\\
(a,0)&\mapsto (f(a),0)\\
(b,1)&\mapsto (g(b),1).
\end{align*}
The tags are essential because they prevent ambiguity between an element coming from $A$ and an element coming from $B$.
To prove that $F$ is bijective, define the candidate inverse by applying the inverse bijections on the corresponding summands:
\begin{align*}
F^{-}:A'\sqcup B'&\to A\sqcup B\\
(a',0)&\mapsto (f^{-1}(a'),0)\\
(b',1)&\mapsto (g^{-1}(b'),1).
\end{align*}
Now compute both composites. For $(a,0)\in A\times\{0\}$,
\begin{align*}
F^{-}(F(a,0))=F^{-}(f(a),0)=(f^{-1}(f(a)),0)=(a,0),
\end{align*}
and for $(b,1)\in B\times\{1\}$,
\begin{align*}
F^{-}(F(b,1))=F^{-}(g(b),1)=(g^{-1}(g(b)),1)=(b,1).
\end{align*}
Therefore $F^{-}\circ F=\operatorname{id}_{A\sqcup B}$. Conversely, for $(a',0)\in A'\times\{0\}$ and $(b',1)\in B'\times\{1\}$,
\begin{align*}
F(F^{-}(a',0))&=F(f^{-1}(a'),0)=(f(f^{-1}(a')),0)=(a',0),\\
F(F^{-}(b',1))&=F(g^{-1}(b'),1)=(g(g^{-1}(b')),1)=(b',1).
\end{align*}
Thus $F\circ F^{-}=\operatorname{id}_{A'\sqcup B'}$. Hence $F$ is a bijection, and the two disjoint unions have the same cardinality.
[/guided]
[/step]
[step:Build a bijection between the Cartesian products]
Define
\begin{align*}
P:A\times B&\to A'\times B'\\
(a,b)&\mapsto (f(a),g(b)).
\end{align*}
Define
\begin{align*}
P^{-}:A'\times B'&\to A\times B\\
(a',b')&\mapsto (f^{-1}(a'),g^{-1}(b')).
\end{align*}
For every $(a,b)\in A\times B$,
\begin{align*}
P^{-}(P(a,b))=P^{-}(f(a),g(b))=(f^{-1}(f(a)),g^{-1}(g(b)))=(a,b).
\end{align*}
For every $(a',b')\in A'\times B'$,
\begin{align*}
P(P^{-}(a',b'))=P(f^{-1}(a'),g^{-1}(b'))=(f(f^{-1}(a')),g(g^{-1}(b')))=(a',b').
\end{align*}
Thus $P$ is a bijection, so $|A\times B|=|A'\times B'|$.
[/step]
[step:Build a bijection between the function sets]
Here $A^B$ denotes the set of all functions $h:B\to A$, and $(A')^{B'}$ denotes the set of all functions $k:B'\to A'$. Define
\begin{align*}
E:A^B&\to (A')^{B'}\\
h&\mapsto f\circ h\circ g^{-1}.
\end{align*}
This is well-defined because $g^{-1}:B'\to B$, $h:B\to A$, and $f:A\to A'$, so $f\circ h\circ g^{-1}:B'\to A'$.
Define
\begin{align*}
E^{-}:(A')^{B'}&\to A^B\\
k&\mapsto f^{-1}\circ k\circ g.
\end{align*}
This is well-defined because $g:B\to B'$, $k:B'\to A'$, and $f^{-1}:A'\to A$, so $f^{-1}\circ k\circ g:B\to A$.
For every $h\in A^B$ and every $b\in B$,
\begin{align*}
(E^{-}(E(h)))(b)
&=(f^{-1}\circ (f\circ h\circ g^{-1})\circ g)(b)\\
&=f^{-1}(f(h(g^{-1}(g(b)))))\\
&=f^{-1}(f(h(b)))\\
&=h(b).
\end{align*}
Hence $E^{-}\circ E=\operatorname{id}_{A^B}$. For every $k\in (A')^{B'}$ and every $b'\in B'$,
\begin{align*}
(E(E^{-}(k)))(b')
&=(f\circ (f^{-1}\circ k\circ g)\circ g^{-1})(b')\\
&=f(f^{-1}(k(g(g^{-1}(b')))))\\
&=f(f^{-1}(k(b')))\\
&=k(b').
\end{align*}
Hence $E\circ E^{-}=\operatorname{id}_{(A')^{B'}}$. Therefore $E$ is a bijection, so $|A^B|=|(A')^{B'}|$.
[guided]
A cardinal exponent $|A|^{|B|}$ is represented by the function set $A^B$, whose elements are functions $h:B\to A$. To transport such a function to a function $B'\to A'$, first move an input $b'\in B'$ back to $B$ using $g^{-1}$, then apply $h$, and finally move the output from $A$ to $A'$ using $f$. This gives the map
\begin{align*}
E:A^B&\to (A')^{B'}\\
h&\mapsto f\circ h\circ g^{-1}.
\end{align*}
The composition has the correct type because
\begin{align*}
B' \xrightarrow{g^{-1}} B \xrightarrow{h} A \xrightarrow{f} A'.
\end{align*}
The inverse operation must reverse this transport. Starting with a function $k:B'\to A'$, define
\begin{align*}
E^{-}:(A')^{B'}&\to A^B\\
k&\mapsto f^{-1}\circ k\circ g.
\end{align*}
This composition has the correct type because
\begin{align*}
B \xrightarrow{g} B' \xrightarrow{k} A' \xrightarrow{f^{-1}} A.
\end{align*}
We now verify that these two constructions undo each other. Let $h\in A^B$. For each $b\in B$,
\begin{align*}
(E^{-}(E(h)))(b)
&=(f^{-1}\circ (f\circ h\circ g^{-1})\circ g)(b)\\
&=f^{-1}(f(h(g^{-1}(g(b)))))\\
&=f^{-1}(f(h(b)))\\
&=h(b).
\end{align*}
Since the two functions $E^{-}(E(h))$ and $h$ agree at every $b\in B$, they are equal as functions $B\to A$. Hence $E^{-}\circ E=\operatorname{id}_{A^B}$.
Conversely, let $k\in (A')^{B'}$. For each $b'\in B'$,
\begin{align*}
(E(E^{-}(k)))(b')
&=(f\circ (f^{-1}\circ k\circ g)\circ g^{-1})(b')\\
&=f(f^{-1}(k(g(g^{-1}(b')))))\\
&=f(f^{-1}(k(b')))\\
&=k(b').
\end{align*}
Thus $E(E^{-}(k))=k$ as functions $B'\to A'$, so $E\circ E^{-}=\operatorname{id}_{(A')^{B'}}$. Therefore $E$ is a bijection, and $A^B$ and $(A')^{B'}$ have the same cardinality.
[/guided]
[/step]
[step:Conclude that the three cardinal operations are independent of representatives]
The preceding steps construct bijections
\begin{align*}
A\sqcup B &\to A'\sqcup B',\\
A\times B &\to A'\times B',\\
A^B &\to (A')^{B'}.
\end{align*}
Therefore
\begin{align*}
|A\sqcup B|&=|A'\sqcup B'|,\\
|A\times B|&=|A'\times B'|,\\
|A^B|&=|(A')^{B'}|.
\end{align*}
Thus cardinal addition, multiplication, and exponentiation are well defined on cardinalities rather than on the particular representative sets.
[/step]
