Definition df-acn

Description: Define a local and length-limited version of the axiom of choice. The definition of the predicate X e. AC_ A is that for all families of nonempty subsets of X indexed on A (i.e. functions A --> ~P X \ { (/) } ), there is a function which selects an element from each set in the family. (Contributed by Mario Carneiro, 31-Aug-2015)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	wacn	⊢ AC 𝐴
2		vx	⊢ 𝑥
3		cvv	⊢ V
4	0 3	wcel	⊢ 𝐴 ∈ V
5		vf	⊢ 𝑓
6	2	cv	⊢ 𝑥
7	6	cpw	⊢ 𝒫 𝑥
8		c0	⊢ ∅
9	8	csn	⊢ { ∅ }
10	7 9	cdif	⊢ ( 𝒫 𝑥 ∖ { ∅ } )
11		cmap	⊢ ↑m
12	10 0 11	co	⊢ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 )
13		vg	⊢ 𝑔
14		vy	⊢ 𝑦
15	13	cv	⊢ 𝑔
16	14	cv	⊢ 𝑦
17	16 15	cfv	⊢ ( 𝑔 ‘ 𝑦 )
18	5	cv	⊢ 𝑓
19	16 18	cfv	⊢ ( 𝑓 ‘ 𝑦 )
20	17 19	wcel	⊢ ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 )
21	20 14 0	wral	⊢ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 )
22	21 13	wex	⊢ ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 )
23	22 5 12	wral	⊢ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 )
24	4 23	wa	⊢ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) )
25	24 2	cab	⊢ { 𝑥 ∣ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) }
26	1 25	wceq	⊢ AC 𝐴 = { 𝑥 ∣ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) }