Definition df-acn 8768

Description: Define a local and length-limited version of the axiom of choice. The definition of the predicate 𝑋 ∈ AC 𝐴 is that for all families of nonempty subsets of 𝑋 indexed on 𝐴 (i.e. functions 𝐴⟶𝒫 𝑋 ∖ {∅}), there is a function which selects an element from each set in the family. (Contributed by Mario Carneiro, 31-Aug-2015.)

Assertion

Ref	Expression
df-acn	⊢ AC 𝐴 = {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))}

Distinct variable group:   𝑓,𝑔,𝑥,𝑦,𝐴

Detailed syntax breakdown of Definition df-acn

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wacn 8764	. 2 class AC 𝐴
3		cvv 3200	. . . . 5 class V
4	1, 3	wcel 1990	. . . 4 wff 𝐴 ∈ V
5		vy	. . . . . . . . . 10 setvar 𝑦
6	5	cv 1482	. . . . . . . . 9 class 𝑦
7		vg	. . . . . . . . . 10 setvar 𝑔
8	7	cv 1482	. . . . . . . . 9 class 𝑔
9	6, 8	cfv 5888	. . . . . . . 8 class (𝑔‘𝑦)
10		vf	. . . . . . . . . 10 setvar 𝑓
11	10	cv 1482	. . . . . . . . 9 class 𝑓
12	6, 11	cfv 5888	. . . . . . . 8 class (𝑓‘𝑦)
13	9, 12	wcel 1990	. . . . . . 7 wff (𝑔‘𝑦) ∈ (𝑓‘𝑦)
14	13, 5, 1	wral 2912	. . . . . 6 wff ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦)
15	14, 7	wex 1704	. . . . 5 wff ∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦)
16		vx	. . . . . . . . 9 setvar 𝑥
17	16	cv 1482	. . . . . . . 8 class 𝑥
18	17	cpw 4158	. . . . . . 7 class 𝒫 𝑥
19		c0 3915	. . . . . . . 8 class ∅
20	19	csn 4177	. . . . . . 7 class {∅}
21	18, 20	cdif 3571	. . . . . 6 class (𝒫 𝑥 ∖ {∅})
22		cmap 7857	. . . . . 6 class ↑𝑚
23	21, 1, 22	co 6650	. . . . 5 class ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)
24	15, 10, 23	wral 2912	. . . 4 wff ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦)
25	4, 24	wa 384	. . 3 wff (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))
26	25, 16	cab 2608	. 2 class {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))}
27	2, 26	wceq 1483	1 wff AC 𝐴 = {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))}

This definition is referenced by:  acnrcl  8865  acneq  8866  isacn  8867