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	⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ↑m 𝐵 ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } )

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( 𝐴 ↑m 𝐵 ) ∈ V
2		numth3	⊢ ( ( 𝐴 ↑m 𝐵 ) ∈ V → ( 𝐴 ↑m 𝐵 ) ∈ dom card )
3	1 2	ax-mp	⊢ ( 𝐴 ↑m 𝐵 ) ∈ dom card
4		infmap2	⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) → ( 𝐴 ↑m 𝐵 ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } )
5	3 4	mp3an3	⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ↑m 𝐵 ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } )