Metamath Proof Explorer

Theorem iunpw

Description: An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of Enderton p. 33. (Contributed by NM, 29-Nov-2003)

Ref Expression
Hypothesis iunpw.1 
|- A e. _V
Assertion iunpw 
|- ( E. x e. A x = U. A <-> ~P U. A = U_ x e. A ~P x )

Proof

Step Hyp Ref Expression
1 iunpw.1 
 |-  A e. _V
2 sseq2 
 |-  ( x = U. A -> ( y C_ x <-> y C_ U. A ) )
3 2 biimprcd 
 |-  ( y C_ U. A -> ( x = U. A -> y C_ x ) )
4 3 reximdv 
 |-  ( y C_ U. A -> ( E. x e. A x = U. A -> E. x e. A y C_ x ) )
5 4 com12 
 |-  ( E. x e. A x = U. A -> ( y C_ U. A -> E. x e. A y C_ x ) )
6 ssiun 
 |-  ( E. x e. A y C_ x -> y C_ U_ x e. A x )
7 uniiun 
 |-  U. A = U_ x e. A x
8 6 7 sseqtrrdi 
 |-  ( E. x e. A y C_ x -> y C_ U. A )
9 5 8 impbid1 
 |-  ( E. x e. A x = U. A -> ( y C_ U. A <-> E. x e. A y C_ x ) )
10 velpw 
 |-  ( y e. ~P U. A <-> y C_ U. A )
11 eliun 
 |-  ( y e. U_ x e. A ~P x <-> E. x e. A y e. ~P x )
12 velpw 
 |-  ( y e. ~P x <-> y C_ x )
13 12 rexbii 
 |-  ( E. x e. A y e. ~P x <-> E. x e. A y C_ x )
14 11 13 bitri 
 |-  ( y e. U_ x e. A ~P x <-> E. x e. A y C_ x )
15 9 10 14 3bitr4g 
 |-  ( E. x e. A x = U. A -> ( y e. ~P U. A <-> y e. U_ x e. A ~P x ) )
16 15 eqrdv 
 |-  ( E. x e. A x = U. A -> ~P U. A = U_ x e. A ~P x )
17 ssid 
 |-  U. A C_ U. A
18 1 uniex 
 |-  U. A e. _V
19 18 elpw 
 |-  ( U. A e. ~P U. A <-> U. A C_ U. A )
20 eleq2 
 |-  ( ~P U. A = U_ x e. A ~P x -> ( U. A e. ~P U. A <-> U. A e. U_ x e. A ~P x ) )
21 19 20 bitr3id 
 |-  ( ~P U. A = U_ x e. A ~P x -> ( U. A C_ U. A <-> U. A e. U_ x e. A ~P x ) )
22 17 21 mpbii 
 |-  ( ~P U. A = U_ x e. A ~P x -> U. A e. U_ x e. A ~P x )
23 eliun 
 |-  ( U. A e. U_ x e. A ~P x <-> E. x e. A U. A e. ~P x )
24 22 23 sylib 
 |-  ( ~P U. A = U_ x e. A ~P x -> E. x e. A U. A e. ~P x )
25 elssuni 
 |-  ( x e. A -> x C_ U. A )
26 elpwi 
 |-  ( U. A e. ~P x -> U. A C_ x )
27 25 26 anim12i 
 |-  ( ( x e. A /\ U. A e. ~P x ) -> ( x C_ U. A /\ U. A C_ x ) )
28 eqss 
 |-  ( x = U. A <-> ( x C_ U. A /\ U. A C_ x ) )
29 27 28 sylibr 
 |-  ( ( x e. A /\ U. A e. ~P x ) -> x = U. A )
30 29 ex 
 |-  ( x e. A -> ( U. A e. ~P x -> x = U. A ) )
31 30 reximia 
 |-  ( E. x e. A U. A e. ~P x -> E. x e. A x = U. A )
32 24 31 syl 
 |-  ( ~P U. A = U_ x e. A ~P x -> E. x e. A x = U. A )
33 16 32 impbii 
 |-  ( E. x e. A x = U. A <-> ~P U. A = U_ x e. A ~P x )