This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) }