# Metamath Proof Explorer

## Theorem ixpssmap2g

Description: An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg avoids ax-rep . (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion ixpssmap2g ${⊢}\bigcup _{{x}\in {A}}{B}\in {V}\to \underset{{x}\in {A}}{⨉}{B}\subseteq {\bigcup _{{x}\in {A}}{B}}^{{A}}$

### Proof

Step Hyp Ref Expression
1 ixpf ${⊢}{f}\in \underset{{x}\in {A}}{⨉}{B}\to {f}:{A}⟶\bigcup _{{x}\in {A}}{B}$
2 1 adantl ${⊢}\left(\bigcup _{{x}\in {A}}{B}\in {V}\wedge {f}\in \underset{{x}\in {A}}{⨉}{B}\right)\to {f}:{A}⟶\bigcup _{{x}\in {A}}{B}$
3 n0i ${⊢}{f}\in \underset{{x}\in {A}}{⨉}{B}\to ¬\underset{{x}\in {A}}{⨉}{B}=\varnothing$
4 ixpprc ${⊢}¬{A}\in \mathrm{V}\to \underset{{x}\in {A}}{⨉}{B}=\varnothing$
5 3 4 nsyl2 ${⊢}{f}\in \underset{{x}\in {A}}{⨉}{B}\to {A}\in \mathrm{V}$
6 elmapg ${⊢}\left(\bigcup _{{x}\in {A}}{B}\in {V}\wedge {A}\in \mathrm{V}\right)\to \left({f}\in \left({\bigcup _{{x}\in {A}}{B}}^{{A}}\right)↔{f}:{A}⟶\bigcup _{{x}\in {A}}{B}\right)$
7 5 6 sylan2 ${⊢}\left(\bigcup _{{x}\in {A}}{B}\in {V}\wedge {f}\in \underset{{x}\in {A}}{⨉}{B}\right)\to \left({f}\in \left({\bigcup _{{x}\in {A}}{B}}^{{A}}\right)↔{f}:{A}⟶\bigcup _{{x}\in {A}}{B}\right)$
8 2 7 mpbird ${⊢}\left(\bigcup _{{x}\in {A}}{B}\in {V}\wedge {f}\in \underset{{x}\in {A}}{⨉}{B}\right)\to {f}\in \left({\bigcup _{{x}\in {A}}{B}}^{{A}}\right)$
9 8 ex ${⊢}\bigcup _{{x}\in {A}}{B}\in {V}\to \left({f}\in \underset{{x}\in {A}}{⨉}{B}\to {f}\in \left({\bigcup _{{x}\in {A}}{B}}^{{A}}\right)\right)$
10 9 ssrdv ${⊢}\bigcup _{{x}\in {A}}{B}\in {V}\to \underset{{x}\in {A}}{⨉}{B}\subseteq {\bigcup _{{x}\in {A}}{B}}^{{A}}$