Higher-Order Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HOLE Home  >  Th. List  >  weu GIF version

Theorem weu 141
 Description: There exists unique type. (Contributed by Mario Carneiro, 8-Oct-2014.)
Assertion
Ref Expression
weu ∃!:((α → ∗) → ∗)

Proof of Theorem weu
Dummy variables p x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wex 139 . . . 4 :((α → ∗) → ∗)
2 wal 134 . . . . . 6 :((α → ∗) → ∗)
3 wv 64 . . . . . . . . 9 p:(α → ∗):(α → ∗)
4 wv 64 . . . . . . . . 9 x:α:α
53, 4wc 50 . . . . . . . 8 (p:(α → ∗)x:α):∗
6 wv 64 . . . . . . . . 9 y:α:α
74, 6weqi 76 . . . . . . . 8 [x:α = y:α]:∗
85, 7weqi 76 . . . . . . 7 [(p:(α → ∗)x:α) = [x:α = y:α]]:∗
98wl 66 . . . . . 6 λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]:(α → ∗)
102, 9wc 50 . . . . 5 (λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]):∗
1110wl 66 . . . 4 λy:α (λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]):(α → ∗)
121, 11wc 50 . . 3 (λy:α (λx:α [(p:(α → ∗)x:α) = [x:α = y:α]])):∗
1312wl 66 . 2 λp:(α → ∗) (λy:α (λx:α [(p:(α → ∗)x:α) = [x:α = y:α]])):((α → ∗) → ∗)
14 df-eu 133 . 2 ⊤⊧[∃! = λp:(α → ∗) (λy:α (λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]))]
1513, 14eqtypri 81 1 ∃!:((α → ∗) → ∗)
 Colors of variables: type var term Syntax hints:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  wffMMJ2t 12  ∀tal 122  ∃tex 123  ∃!teu 125 This theorem was proved from axioms:  ax-cb1 29  ax-weq 40  ax-refl 42  ax-wc 49  ax-wv 63  ax-wl 65  ax-wov 71  ax-eqtypri 80 This theorem depends on definitions:  df-al 126  df-an 128  df-im 129  df-ex 131  df-eu 133 This theorem is referenced by:  euval  144
 Copyright terms: Public domain W3C validator