Step | Hyp | Ref
| Expression |
1 | | sseq2 3171 |
. . . . . . . 8
⊢ (𝑥 = ∪
𝐴 → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ ∪ 𝐴)) |
2 | 1 | biimprcd 159 |
. . . . . . 7
⊢ (𝑦 ⊆ ∪ 𝐴
→ (𝑥 = ∪ 𝐴
→ 𝑦 ⊆ 𝑥)) |
3 | 2 | reximdv 2571 |
. . . . . 6
⊢ (𝑦 ⊆ ∪ 𝐴
→ (∃𝑥 ∈
𝐴 𝑥 = ∪ 𝐴 → ∃𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
4 | 3 | com12 30 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑥 = ∪ 𝐴 → (𝑦 ⊆ ∪ 𝐴 → ∃𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
5 | | ssiun 3915 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 𝑦 ⊆ 𝑥 → 𝑦 ⊆ ∪
𝑥 ∈ 𝐴 𝑥) |
6 | | uniiun 3926 |
. . . . . 6
⊢ ∪ 𝐴 =
∪ 𝑥 ∈ 𝐴 𝑥 |
7 | 5, 6 | sseqtrrdi 3196 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑦 ⊆ 𝑥 → 𝑦 ⊆ ∪ 𝐴) |
8 | 4, 7 | impbid1 141 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 𝑥 = ∪ 𝐴 → (𝑦 ⊆ ∪ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) |
9 | | vex 2733 |
. . . . 5
⊢ 𝑦 ∈ V |
10 | 9 | elpw 3572 |
. . . 4
⊢ (𝑦 ∈ 𝒫 ∪ 𝐴
↔ 𝑦 ⊆ ∪ 𝐴) |
11 | | eliun 3877 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝒫 𝑥) |
12 | | df-pw 3568 |
. . . . . . 7
⊢ 𝒫
𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑥} |
13 | 12 | abeq2i 2281 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 𝑥 ↔ 𝑦 ⊆ 𝑥) |
14 | 13 | rexbii 2477 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑦 ∈ 𝒫 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥) |
15 | 11, 14 | bitri 183 |
. . . 4
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥) |
16 | 8, 10, 15 | 3bitr4g 222 |
. . 3
⊢
(∃𝑥 ∈
𝐴 𝑥 = ∪ 𝐴 → (𝑦 ∈ 𝒫 ∪ 𝐴
↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥)) |
17 | 16 | eqrdv 2168 |
. 2
⊢
(∃𝑥 ∈
𝐴 𝑥 = ∪ 𝐴 → 𝒫 ∪ 𝐴 =
∪ 𝑥 ∈ 𝐴 𝒫 𝑥) |
18 | | ssid 3167 |
. . . . 5
⊢ ∪ 𝐴
⊆ ∪ 𝐴 |
19 | | iunpw.1 |
. . . . . . . 8
⊢ 𝐴 ∈ V |
20 | 19 | uniex 4422 |
. . . . . . 7
⊢ ∪ 𝐴
∈ V |
21 | 20 | elpw 3572 |
. . . . . 6
⊢ (∪ 𝐴
∈ 𝒫 ∪ 𝐴 ↔ ∪ 𝐴 ⊆ ∪ 𝐴) |
22 | | eleq2 2234 |
. . . . . 6
⊢
(𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → (∪ 𝐴 ∈ 𝒫 ∪ 𝐴
↔ ∪ 𝐴 ∈ ∪
𝑥 ∈ 𝐴 𝒫 𝑥)) |
23 | 21, 22 | bitr3id 193 |
. . . . 5
⊢
(𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → (∪ 𝐴 ⊆ ∪ 𝐴
↔ ∪ 𝐴 ∈ ∪
𝑥 ∈ 𝐴 𝒫 𝑥)) |
24 | 18, 23 | mpbii 147 |
. . . 4
⊢
(𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → ∪ 𝐴 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥) |
25 | | eliun 3877 |
. . . 4
⊢ (∪ 𝐴
∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ↔ ∃𝑥 ∈ 𝐴 ∪ 𝐴 ∈ 𝒫 𝑥) |
26 | 24, 25 | sylib 121 |
. . 3
⊢
(𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → ∃𝑥 ∈ 𝐴 ∪ 𝐴 ∈ 𝒫 𝑥) |
27 | | elssuni 3824 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴) |
28 | | elpwi 3575 |
. . . . . . 7
⊢ (∪ 𝐴
∈ 𝒫 𝑥 →
∪ 𝐴 ⊆ 𝑥) |
29 | 27, 28 | anim12i 336 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ ∪ 𝐴 ∈ 𝒫 𝑥) → (𝑥 ⊆ ∪ 𝐴 ∧ ∪ 𝐴
⊆ 𝑥)) |
30 | | eqss 3162 |
. . . . . 6
⊢ (𝑥 = ∪
𝐴 ↔ (𝑥 ⊆ ∪ 𝐴
∧ ∪ 𝐴 ⊆ 𝑥)) |
31 | 29, 30 | sylibr 133 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ ∪ 𝐴 ∈ 𝒫 𝑥) → 𝑥 = ∪ 𝐴) |
32 | 31 | ex 114 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → (∪ 𝐴 ∈ 𝒫 𝑥 → 𝑥 = ∪ 𝐴)) |
33 | 32 | reximia 2565 |
. . 3
⊢
(∃𝑥 ∈
𝐴 ∪ 𝐴
∈ 𝒫 𝑥 →
∃𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴) |
34 | 26, 33 | syl 14 |
. 2
⊢
(𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → ∃𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴) |
35 | 17, 34 | impbii 125 |
1
⊢
(∃𝑥 ∈
𝐴 𝑥 = ∪ 𝐴 ↔ 𝒫 ∪ 𝐴 =
∪ 𝑥 ∈ 𝐴 𝒫 𝑥) |