Step | Hyp | Ref
| Expression |
1 | | wex 139 |
. . 3
⊢ ∃:((α
→ ∗) → ∗) |
2 | | alval.1 |
. . 3
⊢ F:(α
→ ∗) |
3 | 1, 2 | wc 50 |
. 2
⊢ (∃F):∗ |
4 | | df-ex 131 |
. . 3
⊢
⊤⊧[∃ =
λp:(α → ∗) (∀λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗])] |
5 | 1, 2, 4 | ceq1 89 |
. 2
⊢
⊤⊧[(∃F) = (λp:(α
→ ∗) (∀λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗])F)] |
6 | | wal 134 |
. . . 4
⊢ ∀:((∗ → ∗) →
∗) |
7 | | wim 137 |
. . . . . 6
⊢ ⇒ :(∗
→ (∗ → ∗)) |
8 | | wal 134 |
. . . . . . 7
⊢ ∀:((α
→ ∗) → ∗) |
9 | | wv 64 |
. . . . . . . . . 10
⊢ p:(α
→ ∗):(α →
∗) |
10 | | wv 64 |
. . . . . . . . . 10
⊢ x:α:α |
11 | 9, 10 | wc 50 |
. . . . . . . . 9
⊢ (p:(α
→ ∗)x:α):∗ |
12 | | wv 64 |
. . . . . . . . 9
⊢ q:∗:∗ |
13 | 7, 11, 12 | wov 72 |
. . . . . . . 8
⊢ [(p:(α
→ ∗)x:α) ⇒ q:∗]:∗ |
14 | 13 | wl 66 |
. . . . . . 7
⊢
λx:α [(p:(α
→ ∗)x:α) ⇒ q:∗]:(α → ∗) |
15 | 8, 14 | wc 50 |
. . . . . 6
⊢ (∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]):∗ |
16 | 7, 15, 12 | wov 72 |
. . . . 5
⊢ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗]:∗ |
17 | 16 | wl 66 |
. . . 4
⊢
λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗]:(∗ →
∗) |
18 | 6, 17 | wc 50 |
. . 3
⊢ (∀λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗]):∗ |
19 | 9, 2 | weqi 76 |
. . . . . . . . . . 11
⊢ [p:(α
→ ∗) = F]:∗ |
20 | 19 | id 25 |
. . . . . . . . . 10
⊢ [p:(α
→ ∗) = F]⊧[p:(α
→ ∗) = F] |
21 | 9, 10, 20 | ceq1 89 |
. . . . . . . . 9
⊢ [p:(α
→ ∗) = F]⊧[(p:(α
→ ∗)x:α) = (Fx:α)] |
22 | 7, 11, 12, 21 | oveq1 99 |
. . . . . . . 8
⊢ [p:(α
→ ∗) = F]⊧[[(p:(α
→ ∗)x:α) ⇒ q:∗] = [(Fx:α) ⇒ q:∗]] |
23 | 13, 22 | leq 91 |
. . . . . . 7
⊢ [p:(α
→ ∗) = F]⊧[λx:α
[(p:(α → ∗)x:α)
⇒ q:∗] =
λx:α [(Fx:α) ⇒ q:∗]] |
24 | 8, 14, 23 | ceq2 90 |
. . . . . 6
⊢ [p:(α
→ ∗) = F]⊧[(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) = (∀λx:α
[(Fx:α)
⇒ q:∗])] |
25 | 7, 15, 12, 24 | oveq1 99 |
. . . . 5
⊢ [p:(α
→ ∗) = F]⊧[[(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗] = [(∀λx:α
[(Fx:α)
⇒ q:∗]) ⇒ q:∗]] |
26 | 16, 25 | leq 91 |
. . . 4
⊢ [p:(α
→ ∗) = F]⊧[λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗] = λq:∗ [(∀λx:α
[(Fx:α)
⇒ q:∗]) ⇒ q:∗]] |
27 | 6, 17, 26 | ceq2 90 |
. . 3
⊢ [p:(α
→ ∗) = F]⊧[(∀λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗]) = (∀λq:∗ [(∀λx:α
[(Fx:α)
⇒ q:∗]) ⇒ q:∗])] |
28 | 18, 2, 27 | cl 116 |
. 2
⊢
⊤⊧[(λp:(α
→ ∗) (∀λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗])F) =
(∀λq:∗ [(∀λx:α
[(Fx:α)
⇒ q:∗]) ⇒ q:∗])] |
29 | 3, 5, 28 | eqtri 95 |
1
⊢
⊤⊧[(∃F) = (∀λq:∗ [(∀λx:α
[(Fx:α)
⇒ q:∗]) ⇒ q:∗])] |