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	|- ( ( _om ~<_ A /\ B ~<_ A ) -> ( A ^m B ) ~~ { x | ( x C_ A /\ x ~~ B ) } )

Proof

Step	Hyp	Ref	Expression
1		ovex	|- ( A ^m B ) e. _V
2		numth3	|- ( ( A ^m B ) e. _V -> ( A ^m B ) e. dom card )
3	1 2	ax-mp	|- ( A ^m B ) e. dom card
4		infmap2	|- ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) -> ( A ^m B ) ~~ { x | ( x C_ A /\ x ~~ B ) } )
5	3 4	mp3an3	|- ( ( _om ~<_ A /\ B ~<_ A ) -> ( A ^m B ) ~~ { x | ( x C_ A /\ x ~~ B ) } )