Theorem elpwiuncl

Description: Closure of indexed union with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 27-May-2020)

	Ref	Expression
Hypotheses	elpwiuncl.1	$$⊢\phi \to A\in V$$
	elpwiuncl.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in 𝒫C$$
Assertion	elpwiuncl	$$⊢\phi \to \bigcup _{k\in A}B\in 𝒫C$$

Proof

Step	Hyp	Ref	Expression
1		elpwiuncl.1	$$⊢\phi \to A\in V$$
2		elpwiuncl.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in 𝒫C$$
3	2	elpwid	$$⊢\left(\phi \wedge k\in A\right)\to B\subseteq C$$
4	3	ralrimiva	$$⊢\phi \to \forall k\in AB\subseteq C$$
5		iunss	$$⊢\bigcup _{k\in A}B\subseteq C\leftrightarrow \forall k\in AB\subseteq C$$
6	4 5	sylibr	$$⊢\phi \to \bigcup _{k\in A}B\subseteq C$$
7	2	ralrimiva	$$⊢\phi \to \forall k\in AB\in 𝒫C$$
8	1 7	jca	$$⊢\phi \to \left(A\in V\wedge \forall k\in AB\in 𝒫C\right)$$
9		iunexg	$$⊢\left(A\in V\wedge \forall k\in AB\in 𝒫C\right)\to \bigcup _{k\in A}B\in \mathrm{V}$$
10		elpwg	$$⊢\bigcup _{k\in A}B\in \mathrm{V}\to \left(\bigcup _{k\in A}B\in 𝒫C\leftrightarrow \bigcup _{k\in A}B\subseteq C\right)$$
11	8 9 10	3syl	$$⊢\phi \to \left(\bigcup _{k\in A}B\in 𝒫C\leftrightarrow \bigcup _{k\in A}B\subseteq C\right)$$
12	6 11	mpbird	$$⊢\phi \to \bigcup _{k\in A}B\in 𝒫C$$