Proof of Theorem kmlem8
Step | Hyp | Ref
| Expression |
1 | | ralnex 3148 |
. . . . 5
⊢
(∀𝑧 ∈
𝑢 ¬ ∀𝑤 ∈ 𝑧 𝜓 ↔ ¬ ∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓) |
2 | | df-rex 3057 |
. . . . . . . 8
⊢
(∃𝑤 ∈
𝑧 ¬ 𝜓 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ ¬ 𝜓)) |
3 | | rexnal 3150 |
. . . . . . . 8
⊢
(∃𝑤 ∈
𝑧 ¬ 𝜓 ↔ ¬ ∀𝑤 ∈ 𝑧 𝜓) |
4 | 2, 3 | bitr3i 280 |
. . . . . . 7
⊢
(∃𝑤(𝑤 ∈ 𝑧 ∧ ¬ 𝜓) ↔ ¬ ∀𝑤 ∈ 𝑧 𝜓) |
5 | | exsimpl 1876 |
. . . . . . . 8
⊢
(∃𝑤(𝑤 ∈ 𝑧 ∧ ¬ 𝜓) → ∃𝑤 𝑤 ∈ 𝑧) |
6 | | n0 4247 |
. . . . . . . 8
⊢ (𝑧 ≠ ∅ ↔
∃𝑤 𝑤 ∈ 𝑧) |
7 | 5, 6 | sylibr 237 |
. . . . . . 7
⊢
(∃𝑤(𝑤 ∈ 𝑧 ∧ ¬ 𝜓) → 𝑧 ≠ ∅) |
8 | 4, 7 | sylbir 238 |
. . . . . 6
⊢ (¬
∀𝑤 ∈ 𝑧 𝜓 → 𝑧 ≠ ∅) |
9 | 8 | ralimi 3073 |
. . . . 5
⊢
(∀𝑧 ∈
𝑢 ¬ ∀𝑤 ∈ 𝑧 𝜓 → ∀𝑧 ∈ 𝑢 𝑧 ≠ ∅) |
10 | 1, 9 | sylbir 238 |
. . . 4
⊢ (¬
∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 → ∀𝑧 ∈ 𝑢 𝑧 ≠ ∅) |
11 | | kmlem2 9730 |
. . . . 5
⊢
(∃𝑦∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)) ↔ ∃𝑦(¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)))) |
12 | | biimt 364 |
. . . . . . . . 9
⊢ (𝑧 ≠ ∅ →
(∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦) ↔ (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)))) |
13 | 12 | ralimi 3073 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑢 𝑧 ≠ ∅ → ∀𝑧 ∈ 𝑢 (∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦) ↔ (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)))) |
14 | | ralbi 3080 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑢 (∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦) ↔ (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))) → (∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)))) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑢 𝑧 ≠ ∅ → (∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)))) |
16 | 15 | anbi2d 632 |
. . . . . 6
⊢
(∀𝑧 ∈
𝑢 𝑧 ≠ ∅ → ((¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)) ↔ (¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))))) |
17 | 16 | exbidv 1929 |
. . . . 5
⊢
(∀𝑧 ∈
𝑢 𝑧 ≠ ∅ → (∃𝑦(¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)) ↔ ∃𝑦(¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))))) |
18 | 11, 17 | bitr4id 293 |
. . . 4
⊢
(∀𝑧 ∈
𝑢 𝑧 ≠ ∅ → (∃𝑦∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)) ↔ ∃𝑦(¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)))) |
19 | 10, 18 | syl 17 |
. . 3
⊢ (¬
∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 → (∃𝑦∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)) ↔ ∃𝑦(¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)))) |
20 | 19 | pm5.74i 274 |
. 2
⊢ ((¬
∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 → ∃𝑦∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))) ↔ (¬ ∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 → ∃𝑦(¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)))) |
21 | | pm4.64 849 |
. 2
⊢ ((¬
∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 → ∃𝑦(¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))) ↔ (∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 ∨ ∃𝑦(¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)))) |
22 | 20, 21 | bitri 278 |
1
⊢ ((¬
∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 → ∃𝑦∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))) ↔ (∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 ∨ ∃𝑦(¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)))) |