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 ω A B A A B x | x A x B


Step Hyp Ref Expression
1 ovex A B V
2 numth3 A B V A B dom card
3 1 2 ax-mp A B dom card
4 infmap2 ω A B A A B dom card A B x | x A x B
5 3 4 mp3an3 ω A B A A B x | x A x B