Theorem infmap

Description: An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of Jech p. 43. (Contributed by NM, 1-Oct-2004) (Proof shortened by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	infmap	$$⊢\left(\mathrm{\omega }\preccurlyeq A\wedge B\preccurlyeq A\right)\to \left(A^B\right)\approx \left\{x|\left(x\subseteq A\wedge x\approx B\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ovex	$$⊢A^B\in \mathrm{V}$$
2		numth3	$$⊢A^B\in \mathrm{V}\to A^B\in \mathrm{dom}\mathrm{card}$$
3	1 2	ax-mp	$$⊢A^B\in \mathrm{dom}\mathrm{card}$$
4		infmap2	$$⊢\left(\mathrm{\omega }\preccurlyeq A\wedge B\preccurlyeq A\wedge A^B\in \mathrm{dom}\mathrm{card}\right)\to \left(A^B\right)\approx \left\{x|\left(x\subseteq A\wedge x\approx B\right)\right\}$$
5	3 4	mp3an3	$$⊢\left(\mathrm{\omega }\preccurlyeq A\wedge B\preccurlyeq A\right)\to \left(A^B\right)\approx \left\{x|\left(x\subseteq A\wedge x\approx B\right)\right\}$$