Axiom ax-ac 196

Description: Defining property of the indefinite descriptor: it selects an element from any type. This is equivalent to global choice in ZF. (Contributed by Mario Carneiro, 10-Oct-2014.)

Assertion

Ref	Expression
ax-ac	⊢ ⊤⊧(∀λp:(α → ∗) (∀λx:α [(p:(α → ∗)x:α) ⇒ (p:(α → ∗)(εp:(α → ∗)))]))

Distinct variable group:   x,p

Detailed syntax breakdown of Axiom ax-ac

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		tal 122	. . 3 term ∀
3		hal	. . . . 5 type α
4		hb 3	. . . . 5 type ∗
5	3, 4	ht 2	. . . 4 type (α → ∗)
6		vp	. . . 4 var p
7		vx	. . . . . 6 var x
8	5, 6	tv 1	. . . . . . . 8 term p:(α → ∗)
9	3, 7	tv 1	. . . . . . . 8 term x:α
10	8, 9	kc 5	. . . . . . 7 term (p:(α → ∗)x:α)
11		tat 191	. . . . . . . . 9 term ε
12	11, 8	kc 5	. . . . . . . 8 term (εp:(α → ∗))
13	8, 12	kc 5	. . . . . . 7 term (p:(α → ∗)(εp:(α → ∗)))
14		tim 121	. . . . . . 7 term ⇒
15	10, 13, 14	kbr 9	. . . . . 6 term [(p:(α → ∗)x:α) ⇒ (p:(α → ∗)(εp:(α → ∗)))]
16	3, 7, 15	kl 6	. . . . 5 term λx:α [(p:(α → ∗)x:α) ⇒ (p:(α → ∗)(εp:(α → ∗)))]
17	2, 16	kc 5	. . . 4 term (∀λx:α [(p:(α → ∗)x:α) ⇒ (p:(α → ∗)(εp:(α → ∗)))])
18	5, 6, 17	kl 6	. . 3 term λp:(α → ∗) (∀λx:α [(p:(α → ∗)x:α) ⇒ (p:(α → ∗)(εp:(α → ∗)))])
19	2, 18	kc 5	. 2 term (∀λp:(α → ∗) (∀λx:α [(p:(α → ∗)x:α) ⇒ (p:(α → ∗)(εp:(α → ∗)))]))
20	1, 19	wffMMJ2 11	1 wff ⊤⊧(∀λp:(α → ∗) (∀λx:α [(p:(α → ∗)x:α) ⇒ (p:(α → ∗)(εp:(α → ∗)))]))

This axiom is referenced by:  ac  197