This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ixpssmap

Description: An infinite Cartesian product is a subset of set exponentiation. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006)

Ref Expression
Hypothesis ixpssmap.2 ⊢ 𝐵 ∈ V
Assertion ixpssmap X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 )

Proof

Step Hyp Ref Expression
1 ixpssmap.2 ⊢ 𝐵 ∈ V
2 1 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V
3 ixpssmapg ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
4 2 3 ax-mp ⊢ X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 )