# Metamath Proof Explorer

## 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\}$