This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY ZFC Set Theory - add the Axiom of Choice Cardinal number arithmetic using Axiom of Choice 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 𝐵 ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } )