[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'|$.[/step]

[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: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'}|$.[/step]

[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: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]