# Metamath Proof Explorer

## 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 {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}$
5 iunss ${⊢}\bigcup _{{k}\in {A}}{B}\subseteq {C}↔\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}$
6 4 5 sylibr ${⊢}{\phi }\to \bigcup _{{k}\in {A}}{B}\subseteq {C}$
7 2 ralrimiva ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in 𝒫{C}$
8 1 7 jca ${⊢}{\phi }\to \left({A}\in {V}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in 𝒫{C}\right)$
9 iunexg ${⊢}\left({A}\in {V}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}\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}↔\bigcup _{{k}\in {A}}{B}\subseteq {C}\right)$
11 8 9 10 3syl ${⊢}{\phi }\to \left(\bigcup _{{k}\in {A}}{B}\in 𝒫{C}↔\bigcup _{{k}\in {A}}{B}\subseteq {C}\right)$
12 6 11 mpbird ${⊢}{\phi }\to \bigcup _{{k}\in {A}}{B}\in 𝒫{C}$