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

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 
|- ( U_ x e. A B e. V -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )

Proof

Step Hyp Ref Expression
1 ixpf 
 |-  ( f e. X_ x e. A B -> f : A --> U_ x e. A B )
2 1 adantl 
 |-  ( ( U_ x e. A B e. V /\ f e. X_ x e. A B ) -> f : A --> U_ x e. A B )
3 n0i 
 |-  ( f e. X_ x e. A B -> -. X_ x e. A B = (/) )
4 ixpprc 
 |-  ( -. A e. _V -> X_ x e. A B = (/) )
5 3 4 nsyl2 
 |-  ( f e. X_ x e. A B -> A e. _V )
6 elmapg 
 |-  ( ( U_ x e. A B e. V /\ A e. _V ) -> ( f e. ( U_ x e. A B ^m A ) <-> f : A --> U_ x e. A B ) )
7 5 6 sylan2 
 |-  ( ( U_ x e. A B e. V /\ f e. X_ x e. A B ) -> ( f e. ( U_ x e. A B ^m A ) <-> f : A --> U_ x e. A B ) )
8 2 7 mpbird 
 |-  ( ( U_ x e. A B e. V /\ f e. X_ x e. A B ) -> f e. ( U_ x e. A B ^m A ) )
9 8 ex 
 |-  ( U_ x e. A B e. V -> ( f e. X_ x e. A B -> f e. ( U_ x e. A B ^m A ) ) )
10 9 ssrdv 
 |-  ( U_ x e. A B e. V -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )