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