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 ) )