Definition df-acnm 7258

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 inhabited 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.) Change nonempty to inhabited. (Revised by Jim Kingdon, 22-Nov-2025.)

Assertion

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

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

Detailed syntax breakdown of Definition df-acnm

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wacn 7256	. 2 class AC 𝐴
3		cvv 2763	. . . . 5 class V
4	1, 3	wcel 2167	. . . 4 wff 𝐴 ∈ V
5		vy	. . . . . . . . . 10 setvar 𝑦
6	5	cv 1363	. . . . . . . . 9 class 𝑦
7		vg	. . . . . . . . . 10 setvar 𝑔
8	7	cv 1363	. . . . . . . . 9 class 𝑔
9	6, 8	cfv 5259	. . . . . . . 8 class (𝑔‘𝑦)
10		vf	. . . . . . . . . 10 setvar 𝑓
11	10	cv 1363	. . . . . . . . 9 class 𝑓
12	6, 11	cfv 5259	. . . . . . . 8 class (𝑓‘𝑦)
13	9, 12	wcel 2167	. . . . . . 7 wff (𝑔‘𝑦) ∈ (𝑓‘𝑦)
14	13, 5, 1	wral 2475	. . . . . 6 wff ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦)
15	14, 7	wex 1506	. . . . 5 wff ∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦)
16		vj	. . . . . . . . 9 setvar 𝑗
17		vz	. . . . . . . . 9 setvar 𝑧
18	16, 17	wel 2168	. . . . . . . 8 wff 𝑗 ∈ 𝑧
19	18, 16	wex 1506	. . . . . . 7 wff ∃𝑗 𝑗 ∈ 𝑧
20		vx	. . . . . . . . 9 setvar 𝑥
21	20	cv 1363	. . . . . . . 8 class 𝑥
22	21	cpw 3606	. . . . . . 7 class 𝒫 𝑥
23	19, 17, 22	crab 2479	. . . . . 6 class {𝑧 ∈ 𝒫 𝑥 ∣ ∃𝑗 𝑗 ∈ 𝑧}
24		cmap 6716	. . . . . 6 class ↑𝑚
25	23, 1, 24	co 5925	. . . . 5 class ({𝑧 ∈ 𝒫 𝑥 ∣ ∃𝑗 𝑗 ∈ 𝑧} ↑𝑚 𝐴)
26	15, 10, 25	wral 2475	. . . 4 wff ∀𝑓 ∈ ({𝑧 ∈ 𝒫 𝑥 ∣ ∃𝑗 𝑗 ∈ 𝑧} ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦)
27	4, 26	wa 104	. . 3 wff (𝐴 ∈ V ∧ ∀𝑓 ∈ ({𝑧 ∈ 𝒫 𝑥 ∣ ∃𝑗 𝑗 ∈ 𝑧} ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))
28	27, 20	cab 2182	. 2 class {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ({𝑧 ∈ 𝒫 𝑥 ∣ ∃𝑗 𝑗 ∈ 𝑧} ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))}
29	2, 28	wceq 1364	1 wff AC 𝐴 = {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ({𝑧 ∈ 𝒫 𝑥 ∣ ∃𝑗 𝑗 ∈ 𝑧} ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))}

This definition is referenced by:  acnrcl  7284  acneq  7285  isacnm  7286