iunmapsn

Description: The indexed union of set exponentiations to a singleton is equal to the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	iunmapsn.x	$⊢ Ⅎ x φ$
	iunmapsn.a	$⊢ φ \to A \in V$
	iunmapsn.b	$⊢ (φ \land x \in A) \to B \in W$
	iunmapsn.c	$⊢ φ \to C \in Z$
Assertion	iunmapsn	$⊢ φ \to ⋃_{x \in A} (B^{\{C\}}) = {⋃_{x \in A} B}^{\{C\}}$

Proof

Step	Hyp	Ref	Expression
1		iunmapsn.x	$⊢ Ⅎ x φ$
2		iunmapsn.a	$⊢ φ \to A \in V$
3		iunmapsn.b	$⊢ (φ \land x \in A) \to B \in W$
4		iunmapsn.c	$⊢ φ \to C \in Z$
5	1 2 3	iunmapss	$⊢ φ \to ⋃_{x \in A} (B^{\{C\}}) \subseteq {⋃_{x \in A} B}^{\{C\}}$
6		simpr	$⊢ (φ \land f \in ({⋃_{x \in A} B}^{\{C\}})) \to f \in ({⋃_{x \in A} B}^{\{C\}})$
7	3	ex	$⊢ φ \to (x \in A \to B \in W)$
8	1 7	ralrimi	$⊢ φ \to \forall x \in A B \in W$
9		iunexg	$⊢ (A \in V \land \forall x \in A B \in W) \to ⋃_{x \in A} B \in V$
10	2 8 9	syl2anc	$⊢ φ \to ⋃_{x \in A} B \in V$
11	10 4	mapsnd	$⊢ φ \to {⋃_{x \in A} B}^{\{C\}} = \{f \| \exists y \in ⋃_{x \in A} B f = \{⟨C, y⟩\}\}$
12	11	adantr	$⊢ (φ \land f \in ({⋃_{x \in A} B}^{\{C\}})) \to {⋃_{x \in A} B}^{\{C\}} = \{f \| \exists y \in ⋃_{x \in A} B f = \{⟨C, y⟩\}\}$
13	6 12	eleqtrd	$⊢ (φ \land f \in ({⋃_{x \in A} B}^{\{C\}})) \to f \in \{f \| \exists y \in ⋃_{x \in A} B f = \{⟨C, y⟩\}\}$
14		abid	$⊢ f \in \{f \| \exists y \in ⋃_{x \in A} B f = \{⟨C, y⟩\}\} \leftrightarrow \exists y \in ⋃_{x \in A} B f = \{⟨C, y⟩\}$
15	13 14	sylib	$⊢ (φ \land f \in ({⋃_{x \in A} B}^{\{C\}})) \to \exists y \in ⋃_{x \in A} B f = \{⟨C, y⟩\}$
16		eliun	$⊢ y \in ⋃_{x \in A} B \leftrightarrow \exists x \in A y \in B$
17	16	biimpi	$⊢ y \in ⋃_{x \in A} B \to \exists x \in A y \in B$
18	17	3ad2ant2	$⊢ (φ \land y \in ⋃_{x \in A} B \land f = \{⟨C, y⟩\}) \to \exists x \in A y \in B$
19		nfcv	$⊢ \underline{Ⅎ} x y$
20		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} B$
21	19 20	nfel	$⊢ Ⅎ x y \in ⋃_{x \in A} B$
22		nfv	$⊢ Ⅎ x f = \{⟨C, y⟩\}$
23	1 21 22	nf3an	$⊢ Ⅎ x (φ \land y \in ⋃_{x \in A} B \land f = \{⟨C, y⟩\})$
24		rspe	$⊢ (y \in B \land f = \{⟨C, y⟩\}) \to \exists y \in B f = \{⟨C, y⟩\}$
25	24	ancoms	$⊢ (f = \{⟨C, y⟩\} \land y \in B) \to \exists y \in B f = \{⟨C, y⟩\}$
26		abid	$⊢ f \in \{f \| \exists y \in B f = \{⟨C, y⟩\}\} \leftrightarrow \exists y \in B f = \{⟨C, y⟩\}$
27	25 26	sylibr	$⊢ (f = \{⟨C, y⟩\} \land y \in B) \to f \in \{f \| \exists y \in B f = \{⟨C, y⟩\}\}$
28	27	adantll	$⊢ ((φ \land f = \{⟨C, y⟩\}) \land y \in B) \to f \in \{f \| \exists y \in B f = \{⟨C, y⟩\}\}$
29	28	3adant2	$⊢ ((φ \land f = \{⟨C, y⟩\}) \land x \in A \land y \in B) \to f \in \{f \| \exists y \in B f = \{⟨C, y⟩\}\}$
30	4	adantr	$⊢ (φ \land x \in A) \to C \in Z$
31	3 30	mapsnd	$⊢ (φ \land x \in A) \to B^{\{C\}} = \{f \| \exists y \in B f = \{⟨C, y⟩\}\}$
32	31	eqcomd	$⊢ (φ \land x \in A) \to \{f \| \exists y \in B f = \{⟨C, y⟩\}\} = B^{\{C\}}$
33	32	3adant3	$⊢ (φ \land x \in A \land y \in B) \to \{f \| \exists y \in B f = \{⟨C, y⟩\}\} = B^{\{C\}}$
34	33	3adant1r	$⊢ ((φ \land f = \{⟨C, y⟩\}) \land x \in A \land y \in B) \to \{f \| \exists y \in B f = \{⟨C, y⟩\}\} = B^{\{C\}}$
35	29 34	eleqtrd	$⊢ ((φ \land f = \{⟨C, y⟩\}) \land x \in A \land y \in B) \to f \in (B^{\{C\}})$
36	35	3exp	$⊢ (φ \land f = \{⟨C, y⟩\}) \to (x \in A \to (y \in B \to f \in (B^{\{C\}})))$
37	36	3adant2	$⊢ (φ \land y \in ⋃_{x \in A} B \land f = \{⟨C, y⟩\}) \to (x \in A \to (y \in B \to f \in (B^{\{C\}})))$
38	23 37	reximdai	$⊢ (φ \land y \in ⋃_{x \in A} B \land f = \{⟨C, y⟩\}) \to (\exists x \in A y \in B \to \exists x \in A f \in (B^{\{C\}}))$
39	18 38	mpd	$⊢ (φ \land y \in ⋃_{x \in A} B \land f = \{⟨C, y⟩\}) \to \exists x \in A f \in (B^{\{C\}})$
40	39	3exp	$⊢ φ \to (y \in ⋃_{x \in A} B \to (f = \{⟨C, y⟩\} \to \exists x \in A f \in (B^{\{C\}})))$
41	40	rexlimdv	$⊢ φ \to (\exists y \in ⋃_{x \in A} B f = \{⟨C, y⟩\} \to \exists x \in A f \in (B^{\{C\}}))$
42	41	adantr	$⊢ (φ \land f \in ({⋃_{x \in A} B}^{\{C\}})) \to (\exists y \in ⋃_{x \in A} B f = \{⟨C, y⟩\} \to \exists x \in A f \in (B^{\{C\}}))$
43	15 42	mpd	$⊢ (φ \land f \in ({⋃_{x \in A} B}^{\{C\}})) \to \exists x \in A f \in (B^{\{C\}})$
44		eliun	$⊢ f \in ⋃_{x \in A} (B^{\{C\}}) \leftrightarrow \exists x \in A f \in (B^{\{C\}})$
45	43 44	sylibr	$⊢ (φ \land f \in ({⋃_{x \in A} B}^{\{C\}})) \to f \in ⋃_{x \in A} (B^{\{C\}})$
46	5 45	eqelssd	$⊢ φ \to ⋃_{x \in A} (B^{\{C\}}) = {⋃_{x \in A} B}^{\{C\}}$

Metamath Proof Explorer

Theorem iunmapsn

Proof