Theorem ixpssmapc

Description: An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	ixpssmapc.x	|- F/ x ph
	ixpssmapc.c	|- ( ph -> C e. V )
	ixpssmapc.b	|- ( ( ph /\ x e. A ) -> B C_ C )
Assertion	ixpssmapc	|- ( ph -> X_ x e. A B C_ ( C ^m A ) )

Proof

Step	Hyp	Ref	Expression
1		ixpssmapc.x	|- F/ x ph
2		ixpssmapc.c	|- ( ph -> C e. V )
3		ixpssmapc.b	|- ( ( ph /\ x e. A ) -> B C_ C )
4	3	ex	|- ( ph -> ( x e. A -> B C_ C ) )
5	1 4	ralrimi	|- ( ph -> A. x e. A B C_ C )
6		iunss	|- ( U_ x e. A B C_ C <-> A. x e. A B C_ C )
7	5 6	sylibr	|- ( ph -> U_ x e. A B C_ C )
8	2 7	ssexd	|- ( ph -> U_ x e. A B e. _V )
9		ixpssmap2g	|- ( U_ x e. A B e. _V -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
10	8 9	syl	|- ( ph -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
11		mapss	|- ( ( C e. V /\ U_ x e. A B C_ C ) -> ( U_ x e. A B ^m A ) C_ ( C ^m A ) )
12	2 7 11	syl2anc	|- ( ph -> ( U_ x e. A B ^m A ) C_ ( C ^m A ) )
13	10 12	sstrd	|- ( ph -> X_ x e. A B C_ ( C ^m A ) )