Metamath Proof Explorer


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