This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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