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 x φ
iunmapss.a φ A V
iunmapss.b φ x A B W
Assertion iunmapss φ x A B C x A B C

Proof

Step Hyp Ref Expression
1 iunmapss.x x φ
2 iunmapss.a φ A V
3 iunmapss.b φ x A B W
4 3 ex φ x A B W
5 1 4 ralrimi φ x A B W
6 iunexg A V x A B W x A B V
7 2 5 6 syl2anc φ x A B V
8 7 adantr φ x A x A B V
9 ssiun2 x A B x A B
10 9 adantl φ x A B x A B
11 mapss x A B V B x A B B C x A B C
12 8 10 11 syl2anc φ x A B C x A B C
13 12 ex φ x A B C x A B C
14 1 13 ralrimi φ x A B C x A B C
15 nfiu1 _ x x A B
16 nfcv _ x 𝑚
17 nfcv _ x C
18 15 16 17 nfov _ x x A B C
19 18 iunssf x A B C x A B C x A B C x A B C
20 14 19 sylibr φ x A B C x A B C