Step | Hyp | Ref
| Expression |
1 | | wtru 40 |
. . . . . 6
⊢
⊤:∗ |
2 | | wex 129 |
. . . . . . 7
⊢ ∃:(((α
→ ∗) → ∗) → ∗) |
3 | | wan 126 |
. . . . . . . . 9
⊢ ∧ :(∗ → (∗ →
∗)) |
4 | | wv 58 |
. . . . . . . . . 10
⊢ x:(α
→ ∗):(α →
∗) |
5 | | wv 58 |
. . . . . . . . . 10
⊢ z:α:α |
6 | 4, 5 | wc 45 |
. . . . . . . . 9
⊢ (x:(α
→ ∗)z:α):∗ |
7 | | axun.1 |
. . . . . . . . . 10
⊢ A:((α
→ ∗) → ∗) |
8 | 7, 4 | wc 45 |
. . . . . . . . 9
⊢ (Ax:(α →
∗)):∗ |
9 | 3, 6, 8 | wov 64 |
. . . . . . . 8
⊢ [(x:(α
→ ∗)z:α) ∧
(Ax:(α
→ ∗))]:∗ |
10 | 9 | wl 59 |
. . . . . . 7
⊢
λx:(α → ∗) [(x:(α
→ ∗)z:α) ∧
(Ax:(α
→ ∗))]:((α →
∗) → ∗) |
11 | 2, 10 | wc 45 |
. . . . . 6
⊢ (∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]):∗ |
12 | 1, 11 | wct 44 |
. . . . 5
⊢ (⊤, (∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))])):∗ |
13 | 12 | trud 27 |
. . . 4
⊢ (⊤, (∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]))⊧⊤ |
14 | 13 | ex 148 |
. . 3
⊢
⊤⊧[(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ ⊤] |
15 | 14 | alrimiv 141 |
. 2
⊢
⊤⊧(∀λz:α
[(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ ⊤]) |
16 | | wal 124 |
. . . 4
⊢ ∀:((α
→ ∗) → ∗) |
17 | | wim 127 |
. . . . . 6
⊢ ⇒ :(∗
→ (∗ → ∗)) |
18 | | wv 58 |
. . . . . . 7
⊢ y:(α
→ ∗):(α →
∗) |
19 | 18, 5 | wc 45 |
. . . . . 6
⊢ (y:(α
→ ∗)z:α):∗ |
20 | 17, 11, 19 | wov 64 |
. . . . 5
⊢ [(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ (y:(α → ∗)z:α)]:∗ |
21 | 20 | wl 59 |
. . . 4
⊢
λz:α [(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ (y:(α → ∗)z:α)]:(α → ∗) |
22 | 16, 21 | wc 45 |
. . 3
⊢ (∀λz:α
[(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ (y:(α → ∗)z:α)]):∗ |
23 | 1 | wl 59 |
. . 3
⊢
λp:α ⊤:(α → ∗) |
24 | 18, 23 | weqi 68 |
. . . . . . . . 9
⊢ [y:(α
→ ∗) = λp:α ⊤]:∗ |
25 | 24 | id 25 |
. . . . . . . 8
⊢ [y:(α
→ ∗) = λp:α ⊤]⊧[y:(α
→ ∗) = λp:α ⊤] |
26 | 18, 5, 25 | ceq1 79 |
. . . . . . 7
⊢ [y:(α
→ ∗) = λp:α ⊤]⊧[(y:(α
→ ∗)z:α) = (λp:α
⊤z:α)] |
27 | 1, 5, 24 | a17i 96 |
. . . . . . 7
⊢ [y:(α
→ ∗) = λp:α ⊤]⊧[(λp:α
⊤z:α) = ⊤] |
28 | 19, 26, 27 | eqtri 85 |
. . . . . 6
⊢ [y:(α
→ ∗) = λp:α ⊤]⊧[(y:(α
→ ∗)z:α) = ⊤] |
29 | 17, 11, 19, 28 | oveq2 91 |
. . . . 5
⊢ [y:(α
→ ∗) = λp:α ⊤]⊧[[(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ (y:(α → ∗)z:α)] =
[(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ ⊤]] |
30 | 20, 29 | leq 81 |
. . . 4
⊢ [y:(α
→ ∗) = λp:α ⊤]⊧[λz:α
[(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ (y:(α → ∗)z:α)] =
λz:α [(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ ⊤]] |
31 | 16, 21, 30 | ceq2 80 |
. . 3
⊢ [y:(α
→ ∗) = λp:α ⊤]⊧[(∀λz:α
[(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ (y:(α → ∗)z:α)]) =
(∀λz:α
[(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ ⊤])] |
32 | 22, 23, 31 | cla4ev 159 |
. 2
⊢ (∀λz:α
[(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ ⊤])⊧(∃λy:(α
→ ∗) (∀λz:α
[(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ (y:(α → ∗)z:α)])) |
33 | 15, 32 | syl 16 |
1
⊢
⊤⊧(∃λy:(α
→ ∗) (∀λz:α
[(∃λx:(α
→ ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α
→ ∗))]) ⇒ (y:(α → ∗)z:α)])) |