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

Metamath Proof Explorer

Theorem ixpssmapg

Description: An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011)

Ref Expression
Assertion ixpssmapg ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )

Proof

Step Hyp Ref Expression
1 n0i ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → ¬ X 𝑥 ∈ 𝐴 𝐵 = ∅ )
2 ixpprc ⊢ ( ¬ 𝐴 ∈ V → X 𝑥 ∈ 𝐴 𝐵 = ∅ )
3 1 2 nsyl2 ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝐴 ∈ V )
4 id ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 )
5 iunexg ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
6 3 4 5 syl2anr ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
7 ixpssmap2g ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
8 6 7 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
9 simpr ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) → 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 )
10 8 9 sseldd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) → 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
11 10 ex ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) ) )
12 11 ssrdv ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )