Step | Hyp | Ref
| Expression |
1 | | axgroth5 10580 |
. 2
⊢
∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) |
2 | | biid 260 |
. . . 4
⊢ (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦) |
3 | | pweq 4549 |
. . . . . . . . 9
⊢ (𝑧 = 𝑣 → 𝒫 𝑧 = 𝒫 𝑣) |
4 | 3 | sseq1d 3952 |
. . . . . . . 8
⊢ (𝑧 = 𝑣 → (𝒫 𝑧 ⊆ 𝑦 ↔ 𝒫 𝑣 ⊆ 𝑦)) |
5 | 4 | cbvralvw 3383 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑦 𝒫 𝑧 ⊆ 𝑦 ↔ ∀𝑣 ∈ 𝑦 𝒫 𝑣 ⊆ 𝑦) |
6 | | ssid 3943 |
. . . . . . . . . 10
⊢ 𝒫
𝑧 ⊆ 𝒫 𝑧 |
7 | | sseq2 3947 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝒫 𝑧 → (𝒫 𝑧 ⊆ 𝑤 ↔ 𝒫 𝑧 ⊆ 𝒫 𝑧)) |
8 | 7 | rspcev 3561 |
. . . . . . . . . 10
⊢
((𝒫 𝑧 ∈
𝑦 ∧ 𝒫 𝑧 ⊆ 𝒫 𝑧) → ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) |
9 | 6, 8 | mpan2 688 |
. . . . . . . . 9
⊢
(𝒫 𝑧 ∈
𝑦 → ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) |
10 | | pweq 4549 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑤 → 𝒫 𝑣 = 𝒫 𝑤) |
11 | 10 | sseq1d 3952 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑤 → (𝒫 𝑣 ⊆ 𝑦 ↔ 𝒫 𝑤 ⊆ 𝑦)) |
12 | 11 | rspccv 3558 |
. . . . . . . . . . 11
⊢
(∀𝑣 ∈
𝑦 𝒫 𝑣 ⊆ 𝑦 → (𝑤 ∈ 𝑦 → 𝒫 𝑤 ⊆ 𝑦)) |
13 | | pwss 4558 |
. . . . . . . . . . . 12
⊢
(𝒫 𝑤 ⊆
𝑦 ↔ ∀𝑣(𝑣 ⊆ 𝑤 → 𝑣 ∈ 𝑦)) |
14 | | vpwex 5300 |
. . . . . . . . . . . . 13
⊢ 𝒫
𝑧 ∈ V |
15 | | sseq1 3946 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝒫 𝑧 → (𝑣 ⊆ 𝑤 ↔ 𝒫 𝑧 ⊆ 𝑤)) |
16 | | eleq1 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝒫 𝑧 → (𝑣 ∈ 𝑦 ↔ 𝒫 𝑧 ∈ 𝑦)) |
17 | 15, 16 | imbi12d 345 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝒫 𝑧 → ((𝑣 ⊆ 𝑤 → 𝑣 ∈ 𝑦) ↔ (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ∈ 𝑦))) |
18 | 14, 17 | spcv 3544 |
. . . . . . . . . . . 12
⊢
(∀𝑣(𝑣 ⊆ 𝑤 → 𝑣 ∈ 𝑦) → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ∈ 𝑦)) |
19 | 13, 18 | sylbi 216 |
. . . . . . . . . . 11
⊢
(𝒫 𝑤 ⊆
𝑦 → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ∈ 𝑦)) |
20 | 12, 19 | syl6 35 |
. . . . . . . . . 10
⊢
(∀𝑣 ∈
𝑦 𝒫 𝑣 ⊆ 𝑦 → (𝑤 ∈ 𝑦 → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ∈ 𝑦))) |
21 | 20 | rexlimdv 3212 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
𝑦 𝒫 𝑣 ⊆ 𝑦 → (∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ∈ 𝑦)) |
22 | 9, 21 | impbid2 225 |
. . . . . . . 8
⊢
(∀𝑣 ∈
𝑦 𝒫 𝑣 ⊆ 𝑦 → (𝒫 𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤)) |
23 | 22 | ralbidv 3112 |
. . . . . . 7
⊢
(∀𝑣 ∈
𝑦 𝒫 𝑣 ⊆ 𝑦 → (∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ↔ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤)) |
24 | 5, 23 | sylbi 216 |
. . . . . 6
⊢
(∀𝑧 ∈
𝑦 𝒫 𝑧 ⊆ 𝑦 → (∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ↔ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤)) |
25 | 24 | pm5.32i 575 |
. . . . 5
⊢
((∀𝑧 ∈
𝑦 𝒫 𝑧 ⊆ 𝑦 ∧ ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦) ↔ (∀𝑧 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤)) |
26 | | r19.26 3095 |
. . . . 5
⊢
(∀𝑧 ∈
𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦) ↔ (∀𝑧 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑦 ∧ ∀𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦)) |
27 | | r19.26 3095 |
. . . . 5
⊢
(∀𝑧 ∈
𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ↔ (∀𝑧 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤)) |
28 | 25, 26, 27 | 3bitr4i 303 |
. . . 4
⊢
(∀𝑧 ∈
𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦) ↔ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤)) |
29 | | velpw 4538 |
. . . . . 6
⊢ (𝑧 ∈ 𝒫 𝑦 ↔ 𝑧 ⊆ 𝑦) |
30 | | impexp 451 |
. . . . . . . . 9
⊢ (((𝑧 ⊆ 𝑦 ∧ 𝑧 ≼ 𝑦) → (¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦)) ↔ (𝑧 ⊆ 𝑦 → (𝑧 ≼ 𝑦 → (¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦)))) |
31 | | ssdomg 8786 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ V → (𝑧 ⊆ 𝑦 → 𝑧 ≼ 𝑦)) |
32 | 31 | elv 3438 |
. . . . . . . . . . 11
⊢ (𝑧 ⊆ 𝑦 → 𝑧 ≼ 𝑦) |
33 | 32 | pm4.71i 560 |
. . . . . . . . . 10
⊢ (𝑧 ⊆ 𝑦 ↔ (𝑧 ⊆ 𝑦 ∧ 𝑧 ≼ 𝑦)) |
34 | 33 | imbi1i 350 |
. . . . . . . . 9
⊢ ((𝑧 ⊆ 𝑦 → (¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦)) ↔ ((𝑧 ⊆ 𝑦 ∧ 𝑧 ≼ 𝑦) → (¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦))) |
35 | | brsdom 8763 |
. . . . . . . . . . . 12
⊢ (𝑧 ≺ 𝑦 ↔ (𝑧 ≼ 𝑦 ∧ ¬ 𝑧 ≈ 𝑦)) |
36 | 35 | imbi1i 350 |
. . . . . . . . . . 11
⊢ ((𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦) ↔ ((𝑧 ≼ 𝑦 ∧ ¬ 𝑧 ≈ 𝑦) → 𝑧 ∈ 𝑦)) |
37 | | impexp 451 |
. . . . . . . . . . 11
⊢ (((𝑧 ≼ 𝑦 ∧ ¬ 𝑧 ≈ 𝑦) → 𝑧 ∈ 𝑦) ↔ (𝑧 ≼ 𝑦 → (¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦))) |
38 | 36, 37 | bitri 274 |
. . . . . . . . . 10
⊢ ((𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦) ↔ (𝑧 ≼ 𝑦 → (¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦))) |
39 | 38 | imbi2i 336 |
. . . . . . . . 9
⊢ ((𝑧 ⊆ 𝑦 → (𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦)) ↔ (𝑧 ⊆ 𝑦 → (𝑧 ≼ 𝑦 → (¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦)))) |
40 | 30, 34, 39 | 3bitr4ri 304 |
. . . . . . . 8
⊢ ((𝑧 ⊆ 𝑦 → (𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦)) ↔ (𝑧 ⊆ 𝑦 → (¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦))) |
41 | 40 | pm5.74ri 271 |
. . . . . . 7
⊢ (𝑧 ⊆ 𝑦 → ((𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦) ↔ (¬ 𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦))) |
42 | | pm4.64 846 |
. . . . . . 7
⊢ ((¬
𝑧 ≈ 𝑦 → 𝑧 ∈ 𝑦) ↔ (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) |
43 | 41, 42 | bitrdi 287 |
. . . . . 6
⊢ (𝑧 ⊆ 𝑦 → ((𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦) ↔ (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))) |
44 | 29, 43 | sylbi 216 |
. . . . 5
⊢ (𝑧 ∈ 𝒫 𝑦 → ((𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦) ↔ (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))) |
45 | 44 | ralbiia 3091 |
. . . 4
⊢
(∀𝑧 ∈
𝒫 𝑦(𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦) ↔ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) |
46 | 2, 28, 45 | 3anbi123i 1154 |
. . 3
⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦)) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))) |
47 | 46 | exbii 1850 |
. 2
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦)) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))) |
48 | 1, 47 | mpbir 230 |
1
⊢
∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦)) |