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	|- ( ph -> A e. V )
	elpwiuncl.2	|- ( ( ph /\ k e. A ) -> B e. ~P C )
Assertion	elpwiuncl	|- ( ph -> U_ k e. A B e. ~P C )

Proof

Step	Hyp	Ref	Expression
1		elpwiuncl.1	|- ( ph -> A e. V )
2		elpwiuncl.2	|- ( ( ph /\ k e. A ) -> B e. ~P C )
3	2	elpwid	|- ( ( ph /\ k e. A ) -> B C_ C )
4	3	ralrimiva	|- ( ph -> A. k e. A B C_ C )
5		iunss	|- ( U_ k e. A B C_ C <-> A. k e. A B C_ C )
6	4 5	sylibr	|- ( ph -> U_ k e. A B C_ C )
7	2	ralrimiva	|- ( ph -> A. k e. A B e. ~P C )
8	1 7	jca	|- ( ph -> ( A e. V /\ A. k e. A B e. ~P C ) )
9		iunexg	|- ( ( A e. V /\ A. k e. A B e. ~P C ) -> U_ k e. A B e. _V )
10		elpwg	|- ( U_ k e. A B e. _V -> ( U_ k e. A B e. ~P C <-> U_ k e. A B C_ C ) )
11	8 9 10	3syl	|- ( ph -> ( U_ k e. A B e. ~P C <-> U_ k e. A B C_ C ) )
12	6 11	mpbird	|- ( ph -> U_ k e. A B e. ~P C )