Metamath Proof Explorer

Theorem finacn

Description: Every set has finite choice sequences. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion finacn 
|- ( A e. Fin -> AC_ A = _V )

Proof

Step Hyp Ref Expression
1 elmapi 
 |-  ( f e. ( ( ~P x \ { (/) } ) ^m A ) -> f : A --> ( ~P x \ { (/) } ) )
2 1 adantl 
 |-  ( ( A e. Fin /\ f e. ( ( ~P x \ { (/) } ) ^m A ) ) -> f : A --> ( ~P x \ { (/) } ) )
3 ffvelrn 
 |-  ( ( f : A --> ( ~P x \ { (/) } ) /\ y e. A ) -> ( f ` y ) e. ( ~P x \ { (/) } ) )
4 eldifsni 
 |-  ( ( f ` y ) e. ( ~P x \ { (/) } ) -> ( f ` y ) =/= (/) )
5 3 4 syl 
 |-  ( ( f : A --> ( ~P x \ { (/) } ) /\ y e. A ) -> ( f ` y ) =/= (/) )
6 n0 
 |-  ( ( f ` y ) =/= (/) <-> E. z z e. ( f ` y ) )
7 5 6 sylib 
 |-  ( ( f : A --> ( ~P x \ { (/) } ) /\ y e. A ) -> E. z z e. ( f ` y ) )
8 rexv 
 |-  ( E. z e. _V z e. ( f ` y ) <-> E. z z e. ( f ` y ) )
9 7 8 sylibr 
 |-  ( ( f : A --> ( ~P x \ { (/) } ) /\ y e. A ) -> E. z e. _V z e. ( f ` y ) )
10 9 ralrimiva 
 |-  ( f : A --> ( ~P x \ { (/) } ) -> A. y e. A E. z e. _V z e. ( f ` y ) )
11 2 10 syl 
 |-  ( ( A e. Fin /\ f e. ( ( ~P x \ { (/) } ) ^m A ) ) -> A. y e. A E. z e. _V z e. ( f ` y ) )
12 eleq1 
 |-  ( z = ( g ` y ) -> ( z e. ( f ` y ) <-> ( g ` y ) e. ( f ` y ) ) )
13 12 ac6sfi 
 |-  ( ( A e. Fin /\ A. y e. A E. z e. _V z e. ( f ` y ) ) -> E. g ( g : A --> _V /\ A. y e. A ( g ` y ) e. ( f ` y ) ) )
14 11 13 syldan 
 |-  ( ( A e. Fin /\ f e. ( ( ~P x \ { (/) } ) ^m A ) ) -> E. g ( g : A --> _V /\ A. y e. A ( g ` y ) e. ( f ` y ) ) )
15 exsimpr 
 |-  ( E. g ( g : A --> _V /\ A. y e. A ( g ` y ) e. ( f ` y ) ) -> E. g A. y e. A ( g ` y ) e. ( f ` y ) )
16 14 15 syl 
 |-  ( ( A e. Fin /\ f e. ( ( ~P x \ { (/) } ) ^m A ) ) -> E. g A. y e. A ( g ` y ) e. ( f ` y ) )
17 16 ralrimiva 
 |-  ( A e. Fin -> A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) )
18 vex 
 |-  x e. _V
19 isacn 
 |-  ( ( x e. _V /\ A e. Fin ) -> ( x e. AC_ A <-> A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) )
20 18 19 mpan 
 |-  ( A e. Fin -> ( x e. AC_ A <-> A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) )
21 17 20 mpbird 
 |-  ( A e. Fin -> x e. AC_ A )
22 18 a1i 
 |-  ( A e. Fin -> x e. _V )
23 21 22 2thd 
 |-  ( A e. Fin -> ( x e. AC_ A <-> x e. _V ) )
24 23 eqrdv 
 |-  ( A e. Fin -> AC_ A = _V )