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.

Step	Hyp	Ref	Expression
1		wex 139	. . . 4 ⊢ ∃:((α → ∗) → ∗)
2		wal 134	. . . . . 6 ⊢ ∀:((α → ∗) → ∗)
3		wv 64	. . . . . . . . 9 ⊢ p:(α → ∗):(α → ∗)
4		wv 64	. . . . . . . . 9 ⊢ x:α:α
5	3, 4	wc 50	. . . . . . . 8 ⊢ (p:(α → ∗)x:α):∗
6		wv 64	. . . . . . . . 9 ⊢ y:α:α
7	4, 6	weqi 76	. . . . . . . 8 ⊢ [x:α = y:α]:∗
8	5, 7	weqi 76	. . . . . . 7 ⊢ [(p:(α → ∗)x:α) = [x:α = y:α]]:∗
9	8	wl 66	. . . . . 6 ⊢ λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]:(α → ∗)
10	2, 9	wc 50	. . . . 5 ⊢ (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]):∗
11	10	wl 66	. . . 4 ⊢ λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]):(α → ∗)
12	1, 11	wc 50	. . 3 ⊢ (∃λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]])):∗
13	12	wl 66	. 2 ⊢ λp:(α → ∗) (∃λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]])):((α → ∗) → ∗)
14		df-eu 133	. 2 ⊢ ⊤⊧[∃! = λp:(α → ∗) (∃λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]))]
15	13, 14	eqtypri 81	1 ⊢ ∃!:((α → ∗) → ∗)

This proof depends on syntax axioms:  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 proof depends on 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 proof depends on definitions:  df-al 126  df-an 128  df-im 129  df-ex 131  df-eu 133

This theorem is used by:  euval  144