Proof of Theorem zfcndpow
Step | Hyp | Ref
| Expression |
1 | | dtru 5357 |
. . . . 5
⊢ ¬
∀𝑦 𝑦 = 𝑧 |
2 | | exnal 1829 |
. . . . 5
⊢
(∃𝑦 ¬
𝑦 = 𝑧 ↔ ¬ ∀𝑦 𝑦 = 𝑧) |
3 | 1, 2 | mpbir 230 |
. . . 4
⊢
∃𝑦 ¬ 𝑦 = 𝑧 |
4 | | nfe1 2147 |
. . . . 5
⊢
Ⅎ𝑦∃𝑦∀𝑧(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦) |
5 | | axpownd 10367 |
. . . . 5
⊢ (¬
𝑦 = 𝑧 → ∃𝑦∀𝑧(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
6 | 4, 5 | exlimi 2210 |
. . . 4
⊢
(∃𝑦 ¬
𝑦 = 𝑧 → ∃𝑦∀𝑧(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
7 | 3, 6 | ax-mp 5 |
. . 3
⊢
∃𝑦∀𝑧(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦) |
8 | | 19.9v 1987 |
. . . . . . . 8
⊢
(∃𝑥 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧) |
9 | | 19.3v 1985 |
. . . . . . . 8
⊢
(∀𝑧 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥) |
10 | 8, 9 | imbi12i 351 |
. . . . . . 7
⊢
((∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥)) |
11 | 10 | albii 1822 |
. . . . . 6
⊢
(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) ↔ ∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥)) |
12 | 11 | imbi1i 350 |
. . . . 5
⊢
((∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
13 | 12 | albii 1822 |
. . . 4
⊢
(∀𝑧(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧(∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
14 | 13 | exbii 1850 |
. . 3
⊢
(∃𝑦∀𝑧(∀𝑦(∃𝑥 𝑦 ∈ 𝑧 → ∀𝑧 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∃𝑦∀𝑧(∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
15 | 7, 14 | mpbi 229 |
. 2
⊢
∃𝑦∀𝑧(∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦) |
16 | | elequ1 2113 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧)) |
17 | | elequ1 2113 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
18 | 16, 17 | imbi12d 345 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) ↔ (𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥))) |
19 | 18 | cbvalvw 2039 |
. . . . 5
⊢
(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) ↔ ∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥)) |
20 | 19 | imbi1i 350 |
. . . 4
⊢
((∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
21 | 20 | albii 1822 |
. . 3
⊢
(∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧(∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
22 | 21 | exbii 1850 |
. 2
⊢
(∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∃𝑦∀𝑧(∀𝑦(𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑦)) |
23 | 15, 22 | mpbir 230 |
1
⊢
∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) |