Proof of Theorem grothpw
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . . . . . 8
⊢
((𝒫 𝑧
⊆ 𝑦 ∧
∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) → 𝒫 𝑧 ⊆ 𝑦) |
2 | 1 | ralimi 2936 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) → ∀𝑧 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑦) |
3 | | pweq 4111 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → 𝒫 𝑧 = 𝒫 𝑥) |
4 | 3 | sseq1d 3595 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝒫 𝑧 ⊆ 𝑦 ↔ 𝒫 𝑥 ⊆ 𝑦)) |
5 | 4 | rspccv 3279 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑦 𝒫 𝑧 ⊆ 𝑦 → (𝑥 ∈ 𝑦 → 𝒫 𝑥 ⊆ 𝑦)) |
6 | 2, 5 | syl 17 |
. . . . . 6
⊢
(∀𝑧 ∈
𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) → (𝑥 ∈ 𝑦 → 𝒫 𝑥 ⊆ 𝑦)) |
7 | 6 | anim2i 591 |
. . . . 5
⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤)) → (𝑥 ∈ 𝑦 ∧ (𝑥 ∈ 𝑦 → 𝒫 𝑥 ⊆ 𝑦))) |
8 | 7 | 3adant3 1074 |
. . . 4
⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) → (𝑥 ∈ 𝑦 ∧ (𝑥 ∈ 𝑦 → 𝒫 𝑥 ⊆ 𝑦))) |
9 | | pm3.35 609 |
. . . 4
⊢ ((𝑥 ∈ 𝑦 ∧ (𝑥 ∈ 𝑦 → 𝒫 𝑥 ⊆ 𝑦)) → 𝒫 𝑥 ⊆ 𝑦) |
10 | | vex 3176 |
. . . . 5
⊢ 𝑦 ∈ V |
11 | 10 | ssex 4730 |
. . . 4
⊢
(𝒫 𝑥 ⊆
𝑦 → 𝒫 𝑥 ∈ V) |
12 | 8, 9, 11 | 3syl 18 |
. . 3
⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) → 𝒫 𝑥 ∈ V) |
13 | | axgroth5 9525 |
. . 3
⊢
∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) |
14 | 12, 13 | exlimiiv 1846 |
. 2
⊢ 𝒫
𝑥 ∈ V |
15 | | pwidg 4121 |
. . . . 5
⊢
(𝒫 𝑥 ∈
V → 𝒫 𝑥 ∈
𝒫 𝒫 𝑥) |
16 | | pweq 4111 |
. . . . . . 7
⊢ (𝑦 = 𝒫 𝑥 → 𝒫 𝑦 = 𝒫 𝒫 𝑥) |
17 | 16 | eleq2d 2673 |
. . . . . 6
⊢ (𝑦 = 𝒫 𝑥 → (𝒫 𝑥 ∈ 𝒫 𝑦 ↔ 𝒫 𝑥 ∈ 𝒫 𝒫 𝑥)) |
18 | 17 | spcegv 3267 |
. . . . 5
⊢
(𝒫 𝑥 ∈
V → (𝒫 𝑥
∈ 𝒫 𝒫 𝑥 → ∃𝑦𝒫 𝑥 ∈ 𝒫 𝑦)) |
19 | 15, 18 | mpd 15 |
. . . 4
⊢
(𝒫 𝑥 ∈
V → ∃𝑦𝒫
𝑥 ∈ 𝒫 𝑦) |
20 | | elex 3185 |
. . . . 5
⊢
(𝒫 𝑥 ∈
𝒫 𝑦 →
𝒫 𝑥 ∈
V) |
21 | 20 | exlimiv 1845 |
. . . 4
⊢
(∃𝑦𝒫
𝑥 ∈ 𝒫 𝑦 → 𝒫 𝑥 ∈ V) |
22 | 19, 21 | impbii 198 |
. . 3
⊢
(𝒫 𝑥 ∈
V ↔ ∃𝑦𝒫
𝑥 ∈ 𝒫 𝑦) |
23 | 10 | elpw2 4755 |
. . . . 5
⊢
(𝒫 𝑥 ∈
𝒫 𝑦 ↔
𝒫 𝑥 ⊆ 𝑦) |
24 | | pwss 4123 |
. . . . . 6
⊢
(𝒫 𝑥 ⊆
𝑦 ↔ ∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦)) |
25 | | dfss2 3557 |
. . . . . . . 8
⊢ (𝑧 ⊆ 𝑥 ↔ ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)) |
26 | 25 | imbi1i 338 |
. . . . . . 7
⊢ ((𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦) ↔ (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
27 | 26 | albii 1737 |
. . . . . 6
⊢
(∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦) ↔ ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
28 | 24, 27 | bitri 263 |
. . . . 5
⊢
(𝒫 𝑥 ⊆
𝑦 ↔ ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
29 | 23, 28 | bitri 263 |
. . . 4
⊢
(𝒫 𝑥 ∈
𝒫 𝑦 ↔
∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
30 | 29 | exbii 1764 |
. . 3
⊢
(∃𝑦𝒫
𝑥 ∈ 𝒫 𝑦 ↔ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
31 | 22, 30 | bitri 263 |
. 2
⊢
(𝒫 𝑥 ∈
V ↔ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
32 | 14, 31 | mpbi 219 |
1
⊢
∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) |