Metamath Proof Explorer

Theorem acni

Description: The property of being a choice set of length A . (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acni 
|- ( ( X e. AC_ A /\ F : A --> ( ~P X \ { (/) } ) ) -> E. g A. x e. A ( g ` x ) e. ( F ` x ) )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
2 1 eleq2d 
 |-  ( f = F -> ( ( g ` x ) e. ( f ` x ) <-> ( g ` x ) e. ( F ` x ) ) )
3 2 ralbidv 
 |-  ( f = F -> ( A. x e. A ( g ` x ) e. ( f ` x ) <-> A. x e. A ( g ` x ) e. ( F ` x ) ) )
4 3 exbidv 
 |-  ( f = F -> ( E. g A. x e. A ( g ` x ) e. ( f ` x ) <-> E. g A. x e. A ( g ` x ) e. ( F ` x ) ) )
5 acnrcl 
 |-  ( X e. AC_ A -> A e. _V )
6 isacn 
 |-  ( ( X e. AC_ A /\ A e. _V ) -> ( X e. AC_ A <-> A. f e. ( ( ~P X \ { (/) } ) ^m A ) E. g A. x e. A ( g ` x ) e. ( f ` x ) ) )
7 5 6 mpdan 
 |-  ( X e. AC_ A -> ( X e. AC_ A <-> A. f e. ( ( ~P X \ { (/) } ) ^m A ) E. g A. x e. A ( g ` x ) e. ( f ` x ) ) )
8 7 ibi 
 |-  ( X e. AC_ A -> A. f e. ( ( ~P X \ { (/) } ) ^m A ) E. g A. x e. A ( g ` x ) e. ( f ` x ) )
9 8 adantr 
 |-  ( ( X e. AC_ A /\ F : A --> ( ~P X \ { (/) } ) ) -> A. f e. ( ( ~P X \ { (/) } ) ^m A ) E. g A. x e. A ( g ` x ) e. ( f ` x ) )
10 pwexg 
 |-  ( X e. AC_ A -> ~P X e. _V )
11 difexg 
 |-  ( ~P X e. _V -> ( ~P X \ { (/) } ) e. _V )
12 10 11 syl 
 |-  ( X e. AC_ A -> ( ~P X \ { (/) } ) e. _V )
13 12 5 elmapd 
 |-  ( X e. AC_ A -> ( F e. ( ( ~P X \ { (/) } ) ^m A ) <-> F : A --> ( ~P X \ { (/) } ) ) )
14 13 biimpar 
 |-  ( ( X e. AC_ A /\ F : A --> ( ~P X \ { (/) } ) ) -> F e. ( ( ~P X \ { (/) } ) ^m A ) )
15 4 9 14 rspcdva 
 |-  ( ( X e. AC_ A /\ F : A --> ( ~P X \ { (/) } ) ) -> E. g A. x e. A ( g ` x ) e. ( F ` x ) )