This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( 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 )