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 𝐴 ∈ V
Assertion iunpw ( ∃ 𝑥𝐴 𝑥 = 𝐴 ↔ 𝒫 𝐴 = 𝑥𝐴 𝒫 𝑥 )

Proof

Step Hyp Ref Expression
1 iunpw.1 𝐴 ∈ V
2 sseq2 ( 𝑥 = 𝐴 → ( 𝑦𝑥𝑦 𝐴 ) )
3 2 biimprcd ( 𝑦 𝐴 → ( 𝑥 = 𝐴𝑦𝑥 ) )
4 3 reximdv ( 𝑦 𝐴 → ( ∃ 𝑥𝐴 𝑥 = 𝐴 → ∃ 𝑥𝐴 𝑦𝑥 ) )
5 4 com12 ( ∃ 𝑥𝐴 𝑥 = 𝐴 → ( 𝑦 𝐴 → ∃ 𝑥𝐴 𝑦𝑥 ) )
6 ssiun ( ∃ 𝑥𝐴 𝑦𝑥𝑦 𝑥𝐴 𝑥 )
7 uniiun 𝐴 = 𝑥𝐴 𝑥
8 6 7 sseqtrrdi ( ∃ 𝑥𝐴 𝑦𝑥𝑦 𝐴 )
9 5 8 impbid1 ( ∃ 𝑥𝐴 𝑥 = 𝐴 → ( 𝑦 𝐴 ↔ ∃ 𝑥𝐴 𝑦𝑥 ) )
10 velpw ( 𝑦 ∈ 𝒫 𝐴𝑦 𝐴 )
11 eliun ( 𝑦 𝑥𝐴 𝒫 𝑥 ↔ ∃ 𝑥𝐴 𝑦 ∈ 𝒫 𝑥 )
12 velpw ( 𝑦 ∈ 𝒫 𝑥𝑦𝑥 )
13 12 rexbii ( ∃ 𝑥𝐴 𝑦 ∈ 𝒫 𝑥 ↔ ∃ 𝑥𝐴 𝑦𝑥 )
14 11 13 bitri ( 𝑦 𝑥𝐴 𝒫 𝑥 ↔ ∃ 𝑥𝐴 𝑦𝑥 )
15 9 10 14 3bitr4g ( ∃ 𝑥𝐴 𝑥 = 𝐴 → ( 𝑦 ∈ 𝒫 𝐴𝑦 𝑥𝐴 𝒫 𝑥 ) )
16 15 eqrdv ( ∃ 𝑥𝐴 𝑥 = 𝐴 → 𝒫 𝐴 = 𝑥𝐴 𝒫 𝑥 )
17 ssid 𝐴 𝐴
18 1 uniex 𝐴 ∈ V
19 18 elpw ( 𝐴 ∈ 𝒫 𝐴 𝐴 𝐴 )
20 eleq2 ( 𝒫 𝐴 = 𝑥𝐴 𝒫 𝑥 → ( 𝐴 ∈ 𝒫 𝐴 𝐴 𝑥𝐴 𝒫 𝑥 ) )
21 19 20 bitr3id ( 𝒫 𝐴 = 𝑥𝐴 𝒫 𝑥 → ( 𝐴 𝐴 𝐴 𝑥𝐴 𝒫 𝑥 ) )
22 17 21 mpbii ( 𝒫 𝐴 = 𝑥𝐴 𝒫 𝑥 𝐴 𝑥𝐴 𝒫 𝑥 )
23 eliun ( 𝐴 𝑥𝐴 𝒫 𝑥 ↔ ∃ 𝑥𝐴 𝐴 ∈ 𝒫 𝑥 )
24 22 23 sylib ( 𝒫 𝐴 = 𝑥𝐴 𝒫 𝑥 → ∃ 𝑥𝐴 𝐴 ∈ 𝒫 𝑥 )
25 elssuni ( 𝑥𝐴𝑥 𝐴 )
26 elpwi ( 𝐴 ∈ 𝒫 𝑥 𝐴𝑥 )
27 25 26 anim12i ( ( 𝑥𝐴 𝐴 ∈ 𝒫 𝑥 ) → ( 𝑥 𝐴 𝐴𝑥 ) )
28 eqss ( 𝑥 = 𝐴 ↔ ( 𝑥 𝐴 𝐴𝑥 ) )
29 27 28 sylibr ( ( 𝑥𝐴 𝐴 ∈ 𝒫 𝑥 ) → 𝑥 = 𝐴 )
30 29 ex ( 𝑥𝐴 → ( 𝐴 ∈ 𝒫 𝑥𝑥 = 𝐴 ) )
31 30 reximia ( ∃ 𝑥𝐴 𝐴 ∈ 𝒫 𝑥 → ∃ 𝑥𝐴 𝑥 = 𝐴 )
32 24 31 syl ( 𝒫 𝐴 = 𝑥𝐴 𝒫 𝑥 → ∃ 𝑥𝐴 𝑥 = 𝐴 )
33 16 32 impbii ( ∃ 𝑥𝐴 𝑥 = 𝐴 ↔ 𝒫 𝐴 = 𝑥𝐴 𝒫 𝑥 )