Theorem weu 131

Description: There exists unique type.

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 129	. . . 4 ⊢ ∃:((α → ∗) → ∗)
2		wal 124	. . . . . 6 ⊢ ∀:((α → ∗) → ∗)
3		wv 58	. . . . . . . . 9 ⊢ p:(α → ∗):(α → ∗)
4		wv 58	. . . . . . . . 9 ⊢ x:α:α
5	3, 4	wc 45	. . . . . . . 8 ⊢ (p:(α → ∗)x:α):∗
6		wv 58	. . . . . . . . 9 ⊢ y:α:α
7	4, 6	weqi 68	. . . . . . . 8 ⊢ [x:α = y:α]:∗
8	5, 7	weqi 68	. . . . . . 7 ⊢ [(p:(α → ∗)x:α) = [x:α = y:α]]:∗
9	8	wl 59	. . . . . 6 ⊢ λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]:(α → ∗)
10	2, 9	wc 45	. . . . 5 ⊢ (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]):∗
11	10	wl 59	. . . 4 ⊢ λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]):(α → ∗)
12	1, 11	wc 45	. . 3 ⊢ (∃λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]])):∗
13	12	wl 59	. 2 ⊢ λp:(α → ∗) (∃λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]])):((α → ∗) → ∗)
14		df-eu 123	. 2 ⊢ ⊤⊧[∃! = λp:(α → ∗) (∃λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]))]
15	13, 14	eqtypri 71	1 ⊢ ∃!:((α → ∗) → ∗)

Syntax hints:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  wffMMJ2t 12  ∀tal 112  ∃tex 113  ∃!teu 115

This theorem was proved from axioms:  ax-cb1 29  ax-refl 39

This theorem depends on definitions:  df-al 116  df-an 118  df-im 119  df-ex 121  df-eu 123

This theorem is referenced by:  euval  134