Proof of Theorem exnal1
Step | Hyp | Ref
| Expression |
1 | | wex 129 |
. . . 4
⊢ ∃:((α
→ ∗) → ∗) |
2 | | wnot 128 |
. . . . . 6
⊢ ¬ :(∗
→ ∗) |
3 | | alnex1.1 |
. . . . . 6
⊢ A:∗ |
4 | 2, 3 | wc 45 |
. . . . 5
⊢ (¬ A):∗ |
5 | 4 | wl 59 |
. . . 4
⊢
λx:α (¬ A):(α
→ ∗) |
6 | 1, 5 | wc 45 |
. . 3
⊢ (∃λx:α (¬
A)):∗ |
7 | 3 | notnot1 150 |
. . . . . 6
⊢ A⊧(¬ (¬ A)) |
8 | | wtru 40 |
. . . . . 6
⊢
⊤:∗ |
9 | 7, 8 | adantl 51 |
. . . . 5
⊢ (⊤, A)⊧(¬ (¬ A)) |
10 | 9 | alimdv 172 |
. . . 4
⊢ (⊤, (∀λx:α
A))⊧(∀λx:α (¬
(¬ A))) |
11 | | wal 124 |
. . . . . . 7
⊢ ∀:((α
→ ∗) → ∗) |
12 | 2, 4 | wc 45 |
. . . . . . . 8
⊢ (¬ (¬
A)):∗ |
13 | 12 | wl 59 |
. . . . . . 7
⊢
λx:α (¬ (¬ A)):(α
→ ∗) |
14 | 11, 13 | wc 45 |
. . . . . 6
⊢ (∀λx:α (¬
(¬ A))):∗ |
15 | 14 | id 25 |
. . . . 5
⊢ (∀λx:α (¬
(¬ A)))⊧(∀λx:α (¬
(¬ A))) |
16 | 4 | alnex 174 |
. . . . . 6
⊢
⊤⊧[(∀λx:α (¬
(¬ A))) = (¬ (∃λx:α (¬
A)))] |
17 | 14, 16 | a1i 28 |
. . . . 5
⊢ (∀λx:α (¬
(¬ A)))⊧[(∀λx:α (¬
(¬ A))) = (¬ (∃λx:α (¬
A)))] |
18 | 15, 17 | mpbi 72 |
. . . 4
⊢ (∀λx:α (¬
(¬ A)))⊧(¬ (∃λx:α (¬
A))) |
19 | 10, 18 | syl 16 |
. . 3
⊢ (⊤, (∀λx:α
A))⊧(¬ (∃λx:α (¬
A))) |
20 | 6, 19 | con2d 151 |
. 2
⊢ (⊤, (∃λx:α (¬
A)))⊧(¬ (∀λx:α
A)) |
21 | 20 | trul 37 |
1
⊢ (∃λx:α (¬
A))⊧(¬ (∀λx:α
A)) |