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_ A = { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	wacn	|- AC_ A
2		vx	|- x
3		cvv	|- _V
4	0 3	wcel	|- A e. _V
5		vf	|- f
6	2	cv	|- x
7	6	cpw	|- ~P x
8		c0	|- (/)
9	8	csn	|- { (/) }
10	7 9	cdif	|- ( ~P x \ { (/) } )
11		cmap	|- ^m
12	10 0 11	co	|- ( ( ~P x \ { (/) } ) ^m A )
13		vg	|- g
14		vy	|- y
15	13	cv	|- g
16	14	cv	|- y
17	16 15	cfv	|- ( g ` y )
18	5	cv	|- f
19	16 18	cfv	|- ( f ` y )
20	17 19	wcel	|- ( g ` y ) e. ( f ` y )
21	20 14 0	wral	|- A. y e. A ( g ` y ) e. ( f ` y )
22	21 13	wex	|- E. g A. y e. A ( g ` y ) e. ( f ` y )
23	22 5 12	wral	|- A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y )
24	4 23	wa	|- ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) )
25	24 2	cab	|- { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }
26	1 25	wceq	|- AC_ A = { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }