Step | Hyp | Ref
| Expression |
1 | | ax-pow 5242 |
. . 3
⊢
∃𝑥∀𝑦(∀𝑧(𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣) → 𝑦 ∈ 𝑥) |
2 | | df-ral 3059 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑦 ∀𝑤 ¬ 𝑤 ∈ 𝑧 ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤 ¬ 𝑤 ∈ 𝑧)) |
3 | | imim2 58 |
. . . . . . . 8
⊢
((∀𝑤 ¬
𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣) → ((𝑧 ∈ 𝑦 → ∀𝑤 ¬ 𝑤 ∈ 𝑧) → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣))) |
4 | 3 | al2imi 1822 |
. . . . . . 7
⊢
(∀𝑧(∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣) → (∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤 ¬ 𝑤 ∈ 𝑧) → ∀𝑧(𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣))) |
5 | 2, 4 | syl5bi 245 |
. . . . . 6
⊢
(∀𝑧(∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣) → (∀𝑧 ∈ 𝑦 ∀𝑤 ¬ 𝑤 ∈ 𝑧 → ∀𝑧(𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣))) |
6 | 5 | imim1d 82 |
. . . . 5
⊢
(∀𝑧(∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣) → ((∀𝑧(𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣) → 𝑦 ∈ 𝑥) → (∀𝑧 ∈ 𝑦 ∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥))) |
7 | 6 | alimdv 1923 |
. . . 4
⊢
(∀𝑧(∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣) → (∀𝑦(∀𝑧(𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣) → 𝑦 ∈ 𝑥) → ∀𝑦(∀𝑧 ∈ 𝑦 ∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥))) |
8 | 7 | eximdv 1924 |
. . 3
⊢
(∀𝑧(∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣) → (∃𝑥∀𝑦(∀𝑧(𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣) → 𝑦 ∈ 𝑥) → ∃𝑥∀𝑦(∀𝑧 ∈ 𝑦 ∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥))) |
9 | 1, 8 | mpi 20 |
. 2
⊢
(∀𝑧(∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣) → ∃𝑥∀𝑦(∀𝑧 ∈ 𝑦 ∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥)) |
10 | | axprlem1 5300 |
. 2
⊢
∃𝑣∀𝑧(∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣) |
11 | 9, 10 | exlimiiv 1938 |
1
⊢
∃𝑥∀𝑦(∀𝑧 ∈ 𝑦 ∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥) |