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	⊢ Ⅎ 𝑥 𝜑
	iunmapss.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	iunmapss.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
Assertion	iunmapss	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		iunmapss.x	⊢ Ⅎ 𝑥 𝜑
2		iunmapss.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		iunmapss.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
4	3	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑊 ) )
5	1 4	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 )
6		iunexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
7	2 5 6	syl2anc	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
8	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
9		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
11		mapss	⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V ∧ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( 𝐵 ↑m 𝐶 ) ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶 ) )
12	8 10 11	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ↑m 𝐶 ) ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶 ) )
13	12	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝐵 ↑m 𝐶 ) ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶 ) ) )
14	1 13	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶 ) )
15		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
16		nfcv	⊢ Ⅎ 𝑥 ↑m
17		nfcv	⊢ Ⅎ 𝑥 𝐶
18	15 16 17	nfov	⊢ Ⅎ 𝑥 ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶 )
19	18	iunssf	⊢ ( ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶 ) )
20	14 19	sylibr	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶 ) )