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 
|- ( A. 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 n0i 
 |-  ( f e. X_ x e. A B -> -. X_ x e. A B = (/) )
2 ixpprc 
 |-  ( -. A e. _V -> X_ x e. A B = (/) )
3 1 2 nsyl2 
 |-  ( f e. X_ x e. A B -> A e. _V )
4 id 
 |-  ( A. x e. A B e. V -> A. x e. A B e. V )
5 iunexg 
 |-  ( ( A e. _V /\ A. x e. A B e. V ) -> U_ x e. A B e. _V )
6 3 4 5 syl2anr 
 |-  ( ( A. x e. A B e. V /\ f e. X_ x e. A B ) -> U_ x e. A B e. _V )
7 ixpssmap2g 
 |-  ( U_ x e. A B e. _V -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
8 6 7 syl 
 |-  ( ( A. x e. A B e. V /\ f e. X_ x e. A B ) -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
9 simpr 
 |-  ( ( A. x e. A B e. V /\ f e. X_ x e. A B ) -> f e. X_ x e. A B )
10 8 9 sseldd 
 |-  ( ( A. x e. A B e. V /\ f e. X_ x e. A B ) -> f e. ( U_ x e. A B ^m A ) )
11 10 ex 
 |-  ( A. x e. A B e. V -> ( f e. X_ x e. A B -> f e. ( U_ x e. A B ^m A ) ) )
12 11 ssrdv 
 |-  ( A. x e. A B e. V -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )