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	$⊢ φ \to A \in V$
	iunmapss.b	$⊢ (φ \land x \in A) \to B \in W$
Assertion	iunmapss	$⊢ φ \to ⋃_{x \in A} (B^{C}) \subseteq {⋃_{x \in A} B}^{C}$

Proof

Step	Hyp	Ref	Expression
1		iunmapss.x	$⊢ Ⅎ x φ$
2		iunmapss.a	$⊢ φ \to A \in V$
3		iunmapss.b	$⊢ (φ \land x \in A) \to B \in W$
4	3	ex	$⊢ φ \to (x \in A \to B \in W)$
5	1 4	ralrimi	$⊢ φ \to \forall x \in A B \in W$
6		iunexg	$⊢ (A \in V \land \forall x \in A B \in W) \to ⋃_{x \in A} B \in V$
7	2 5 6	syl2anc	$⊢ φ \to ⋃_{x \in A} B \in V$
8	7	adantr	$⊢ (φ \land x \in A) \to ⋃_{x \in A} B \in V$
9		ssiun2	$⊢ x \in A \to B \subseteq ⋃_{x \in A} B$
10	9	adantl	$⊢ (φ \land x \in A) \to B \subseteq ⋃_{x \in A} B$
11		mapss	$⊢ (⋃_{x \in A} B \in V \land B \subseteq ⋃_{x \in A} B) \to B^{C} \subseteq {⋃_{x \in A} B}^{C}$
12	8 10 11	syl2anc	$⊢ (φ \land x \in A) \to B^{C} \subseteq {⋃_{x \in A} B}^{C}$
13	12	ex	$⊢ φ \to (x \in A \to B^{C} \subseteq {⋃_{x \in A} B}^{C})$
14	1 13	ralrimi	$⊢ φ \to \forall x \in A B^{C} \subseteq {⋃_{x \in A} B}^{C}$
15		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} B$
16		nfcv	$⊢ \underline{Ⅎ} x ↑_{𝑚}$
17		nfcv	$⊢ \underline{Ⅎ} x C$
18	15 16 17	nfov	$⊢ \underline{Ⅎ} x ({⋃_{x \in A} B}^{C})$
19	18	iunssf	$⊢ ⋃_{x \in A} (B^{C}) \subseteq {⋃_{x \in A} B}^{C} \leftrightarrow \forall x \in A B^{C} \subseteq {⋃_{x \in A} B}^{C}$
20	14 19	sylibr	$⊢ φ \to ⋃_{x \in A} (B^{C}) \subseteq {⋃_{x \in A} B}^{C}$

Metamath Proof Explorer

Theorem iunmapss

Proof