Definition df-acn 9709

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 ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑m 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))}

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

Detailed syntax breakdown of Definition df-acn

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wacn 9705	. 2 class AC 𝐴
3		cvv 3433	. . . . 5 class V
4	1, 3	wcel 2107	. . . 4 wff 𝐴 ∈ V
5		vy	. . . . . . . . . 10 setvar 𝑦
6	5	cv 1538	. . . . . . . . 9 class 𝑦
7		vg	. . . . . . . . . 10 setvar 𝑔
8	7	cv 1538	. . . . . . . . 9 class 𝑔
9	6, 8	cfv 6437	. . . . . . . 8 class (𝑔‘𝑦)
10		vf	. . . . . . . . . 10 setvar 𝑓
11	10	cv 1538	. . . . . . . . 9 class 𝑓
12	6, 11	cfv 6437	. . . . . . . 8 class (𝑓‘𝑦)
13	9, 12	wcel 2107	. . . . . . 7 wff (𝑔‘𝑦) ∈ (𝑓‘𝑦)
14	13, 5, 1	wral 3065	. . . . . 6 wff ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦)
15	14, 7	wex 1782	. . . . 5 wff ∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦)
16		vx	. . . . . . . . 9 setvar 𝑥
17	16	cv 1538	. . . . . . . 8 class 𝑥
18	17	cpw 4534	. . . . . . 7 class 𝒫 𝑥
19		c0 4257	. . . . . . . 8 class ∅
20	19	csn 4562	. . . . . . 7 class {∅}
21	18, 20	cdif 3885	. . . . . 6 class (𝒫 𝑥 ∖ {∅})
22		cmap 8624	. . . . . 6 class ↑m
23	21, 1, 22	co 7284	. . . . 5 class ((𝒫 𝑥 ∖ {∅}) ↑m 𝐴)
24	15, 10, 23	wral 3065	. . . 4 wff ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑m 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦)
25	4, 24	wa 396	. . 3 wff (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑m 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))
26	25, 16	cab 2716	. 2 class {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑m 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))}
27	2, 26	wceq 1539	1 wff AC 𝐴 = {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑m 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))}

This definition is referenced by:  acnrcl  9807  acneq  9808  isacn  9809