Theorem iunmapss

Description: The indexed union of set exponentiations is a subset of the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	iunmapss.x	|- F/ x ph
	iunmapss.a	|- ( ph -> A e. V )
	iunmapss.b	|- ( ( ph /\ x e. A ) -> B e. W )
Assertion	iunmapss	|- ( ph -> U_ x e. A ( B ^m C ) C_ ( U_ x e. A B ^m C ) )

Proof

Step	Hyp	Ref	Expression
1		iunmapss.x	|- F/ x ph
2		iunmapss.a	|- ( ph -> A e. V )
3		iunmapss.b	|- ( ( ph /\ x e. A ) -> B e. W )
4	3	ex	|- ( ph -> ( x e. A -> B e. W ) )
5	1 4	ralrimi	|- ( ph -> A. x e. A B e. W )
6		iunexg	|- ( ( A e. V /\ A. x e. A B e. W ) -> U_ x e. A B e. _V )
7	2 5 6	syl2anc	|- ( ph -> U_ x e. A B e. _V )
8	7	adantr	|- ( ( ph /\ x e. A ) -> U_ x e. A B e. _V )
9		ssiun2	|- ( x e. A -> B C_ U_ x e. A B )
10	9	adantl	|- ( ( ph /\ x e. A ) -> B C_ U_ x e. A B )
11		mapss	|- ( ( U_ x e. A B e. _V /\ B C_ U_ x e. A B ) -> ( B ^m C ) C_ ( U_ x e. A B ^m C ) )
12	8 10 11	syl2anc	|- ( ( ph /\ x e. A ) -> ( B ^m C ) C_ ( U_ x e. A B ^m C ) )
13	12	ex	|- ( ph -> ( x e. A -> ( B ^m C ) C_ ( U_ x e. A B ^m C ) ) )
14	1 13	ralrimi	|- ( ph -> A. x e. A ( B ^m C ) C_ ( U_ x e. A B ^m C ) )
15		nfiu1	|- F/_ x U_ x e. A B
16		nfcv	|- F/_ x ^m
17		nfcv	|- F/_ x C
18	15 16 17	nfov	|- F/_ x ( U_ x e. A B ^m C )
19	18	iunssf	|- ( U_ x e. A ( B ^m C ) C_ ( U_ x e. A B ^m C ) <-> A. x e. A ( B ^m C ) C_ ( U_ x e. A B ^m C ) )
20	14 19	sylibr	|- ( ph -> U_ x e. A ( B ^m C ) C_ ( U_ x e. A B ^m C ) )