Metamath Proof Explorer

Theorem acni2

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

Ref Expression
Assertion acni2 
|- ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) -> E. g ( g : A --> X /\ A. x e. A ( g ` x ) e. B ) )

Proof

Step Hyp Ref Expression
1 eldifsn 
 |-  ( B e. ( ~P X \ { (/) } ) <-> ( B e. ~P X /\ B =/= (/) ) )
2 elpw2g 
 |-  ( X e. AC_ A -> ( B e. ~P X <-> B C_ X ) )
3 2 anbi1d 
 |-  ( X e. AC_ A -> ( ( B e. ~P X /\ B =/= (/) ) <-> ( B C_ X /\ B =/= (/) ) ) )
4 1 3 bitrid 
 |-  ( X e. AC_ A -> ( B e. ( ~P X \ { (/) } ) <-> ( B C_ X /\ B =/= (/) ) ) )
5 4 ralbidv 
 |-  ( X e. AC_ A -> ( A. x e. A B e. ( ~P X \ { (/) } ) <-> A. x e. A ( B C_ X /\ B =/= (/) ) ) )
6 5 biimpar 
 |-  ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) -> A. x e. A B e. ( ~P X \ { (/) } ) )
7 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
8 7 fmpt 
 |-  ( A. x e. A B e. ( ~P X \ { (/) } ) <-> ( x e. A |-> B ) : A --> ( ~P X \ { (/) } ) )
9 6 8 sylib 
 |-  ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) -> ( x e. A |-> B ) : A --> ( ~P X \ { (/) } ) )
10 acni 
 |-  ( ( X e. AC_ A /\ ( x e. A |-> B ) : A --> ( ~P X \ { (/) } ) ) -> E. f A. y e. A ( f ` y ) e. ( ( x e. A |-> B ) ` y ) )
11 9 10 syldan 
 |-  ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) -> E. f A. y e. A ( f ` y ) e. ( ( x e. A |-> B ) ` y ) )
12 nffvmpt1 
 |-  F/_ x ( ( x e. A |-> B ) ` y )
13 12 nfel2 
 |-  F/ x ( f ` y ) e. ( ( x e. A |-> B ) ` y )
14 nfv 
 |-  F/ y ( f ` x ) e. ( ( x e. A |-> B ) ` x )
15 fveq2 
 |-  ( y = x -> ( f ` y ) = ( f ` x ) )
16 fveq2 
 |-  ( y = x -> ( ( x e. A |-> B ) ` y ) = ( ( x e. A |-> B ) ` x ) )
17 15 16 eleq12d 
 |-  ( y = x -> ( ( f ` y ) e. ( ( x e. A |-> B ) ` y ) <-> ( f ` x ) e. ( ( x e. A |-> B ) ` x ) ) )
18 13 14 17 cbvralw 
 |-  ( A. y e. A ( f ` y ) e. ( ( x e. A |-> B ) ` y ) <-> A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) )
19 simplr 
 |-  ( ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) /\ A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) ) -> A. x e. A ( B C_ X /\ B =/= (/) ) )
20 simplr 
 |-  ( ( ( X e. AC_ A /\ x e. A ) /\ B C_ X ) -> x e. A )
21 simpll 
 |-  ( ( ( X e. AC_ A /\ x e. A ) /\ B C_ X ) -> X e. AC_ A )
22 simpr 
 |-  ( ( ( X e. AC_ A /\ x e. A ) /\ B C_ X ) -> B C_ X )
23 21 22 ssexd 
 |-  ( ( ( X e. AC_ A /\ x e. A ) /\ B C_ X ) -> B e. _V )
24 7 fvmpt2 
 |-  ( ( x e. A /\ B e. _V ) -> ( ( x e. A |-> B ) ` x ) = B )
25 20 23 24 syl2anc 
 |-  ( ( ( X e. AC_ A /\ x e. A ) /\ B C_ X ) -> ( ( x e. A |-> B ) ` x ) = B )
26 25 eleq2d 
 |-  ( ( ( X e. AC_ A /\ x e. A ) /\ B C_ X ) -> ( ( f ` x ) e. ( ( x e. A |-> B ) ` x ) <-> ( f ` x ) e. B ) )
27 26 ex 
 |-  ( ( X e. AC_ A /\ x e. A ) -> ( B C_ X -> ( ( f ` x ) e. ( ( x e. A |-> B ) ` x ) <-> ( f ` x ) e. B ) ) )
28 27 adantrd 
 |-  ( ( X e. AC_ A /\ x e. A ) -> ( ( B C_ X /\ B =/= (/) ) -> ( ( f ` x ) e. ( ( x e. A |-> B ) ` x ) <-> ( f ` x ) e. B ) ) )
29 28 ralimdva 
 |-  ( X e. AC_ A -> ( A. x e. A ( B C_ X /\ B =/= (/) ) -> A. x e. A ( ( f ` x ) e. ( ( x e. A |-> B ) ` x ) <-> ( f ` x ) e. B ) ) )
30 29 imp 
 |-  ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) -> A. x e. A ( ( f ` x ) e. ( ( x e. A |-> B ) ` x ) <-> ( f ` x ) e. B ) )
31 ralbi 
 |-  ( A. x e. A ( ( f ` x ) e. ( ( x e. A |-> B ) ` x ) <-> ( f ` x ) e. B ) -> ( A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) <-> A. x e. A ( f ` x ) e. B ) )
32 30 31 syl 
 |-  ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) -> ( A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) <-> A. x e. A ( f ` x ) e. B ) )
33 32 biimpa 
 |-  ( ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) /\ A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) ) -> A. x e. A ( f ` x ) e. B )
34 ssel 
 |-  ( B C_ X -> ( ( f ` x ) e. B -> ( f ` x ) e. X ) )
35 34 adantr 
 |-  ( ( B C_ X /\ B =/= (/) ) -> ( ( f ` x ) e. B -> ( f ` x ) e. X ) )
36 35 ral2imi 
 |-  ( A. x e. A ( B C_ X /\ B =/= (/) ) -> ( A. x e. A ( f ` x ) e. B -> A. x e. A ( f ` x ) e. X ) )
37 19 33 36 sylc 
 |-  ( ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) /\ A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) ) -> A. x e. A ( f ` x ) e. X )
38 fveq2 
 |-  ( x = y -> ( f ` x ) = ( f ` y ) )
39 38 eleq1d 
 |-  ( x = y -> ( ( f ` x ) e. X <-> ( f ` y ) e. X ) )
40 39 rspccva 
 |-  ( ( A. x e. A ( f ` x ) e. X /\ y e. A ) -> ( f ` y ) e. X )
41 37 40 sylan 
 |-  ( ( ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) /\ A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) ) /\ y e. A ) -> ( f ` y ) e. X )
42 41 fmpttd 
 |-  ( ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) /\ A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) ) -> ( y e. A |-> ( f ` y ) ) : A --> X )
43 simpll 
 |-  ( ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) /\ A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) ) -> X e. AC_ A )
44 acnrcl 
 |-  ( X e. AC_ A -> A e. _V )
45 43 44 syl 
 |-  ( ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) /\ A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) ) -> A e. _V )
46 fex2 
 |-  ( ( ( y e. A |-> ( f ` y ) ) : A --> X /\ A e. _V /\ X e. AC_ A ) -> ( y e. A |-> ( f ` y ) ) e. _V )
47 42 45 43 46 syl3anc 
 |-  ( ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) /\ A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) ) -> ( y e. A |-> ( f ` y ) ) e. _V )
48 eqid 
 |-  ( y e. A |-> ( f ` y ) ) = ( y e. A |-> ( f ` y ) )
49 fvex 
 |-  ( f ` x ) e. _V
50 15 48 49 fvmpt 
 |-  ( x e. A -> ( ( y e. A |-> ( f ` y ) ) ` x ) = ( f ` x ) )
51 50 eleq1d 
 |-  ( x e. A -> ( ( ( y e. A |-> ( f ` y ) ) ` x ) e. B <-> ( f ` x ) e. B ) )
52 51 ralbiia 
 |-  ( A. x e. A ( ( y e. A |-> ( f ` y ) ) ` x ) e. B <-> A. x e. A ( f ` x ) e. B )
53 33 52 sylibr 
 |-  ( ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) /\ A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) ) -> A. x e. A ( ( y e. A |-> ( f ` y ) ) ` x ) e. B )
54 42 53 jca 
 |-  ( ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) /\ A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) ) -> ( ( y e. A |-> ( f ` y ) ) : A --> X /\ A. x e. A ( ( y e. A |-> ( f ` y ) ) ` x ) e. B ) )
55 feq1 
 |-  ( g = ( y e. A |-> ( f ` y ) ) -> ( g : A --> X <-> ( y e. A |-> ( f ` y ) ) : A --> X ) )
56 fveq1 
 |-  ( g = ( y e. A |-> ( f ` y ) ) -> ( g ` x ) = ( ( y e. A |-> ( f ` y ) ) ` x ) )
57 56 eleq1d 
 |-  ( g = ( y e. A |-> ( f ` y ) ) -> ( ( g ` x ) e. B <-> ( ( y e. A |-> ( f ` y ) ) ` x ) e. B ) )
58 57 ralbidv 
 |-  ( g = ( y e. A |-> ( f ` y ) ) -> ( A. x e. A ( g ` x ) e. B <-> A. x e. A ( ( y e. A |-> ( f ` y ) ) ` x ) e. B ) )
59 55 58 anbi12d 
 |-  ( g = ( y e. A |-> ( f ` y ) ) -> ( ( g : A --> X /\ A. x e. A ( g ` x ) e. B ) <-> ( ( y e. A |-> ( f ` y ) ) : A --> X /\ A. x e. A ( ( y e. A |-> ( f ` y ) ) ` x ) e. B ) ) )
60 47 54 59 spcedv 
 |-  ( ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) /\ A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) ) -> E. g ( g : A --> X /\ A. x e. A ( g ` x ) e. B ) )
61 60 ex 
 |-  ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) -> ( A. x e. A ( f ` x ) e. ( ( x e. A |-> B ) ` x ) -> E. g ( g : A --> X /\ A. x e. A ( g ` x ) e. B ) ) )
62 18 61 syl5bi 
 |-  ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) -> ( A. y e. A ( f ` y ) e. ( ( x e. A |-> B ) ` y ) -> E. g ( g : A --> X /\ A. x e. A ( g ` x ) e. B ) ) )
63 62 exlimdv 
 |-  ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) -> ( E. f A. y e. A ( f ` y ) e. ( ( x e. A |-> B ) ` y ) -> E. g ( g : A --> X /\ A. x e. A ( g ` x ) e. B ) ) )
64 11 63 mpd 
 |-  ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) -> E. g ( g : A --> X /\ A. x e. A ( g ` x ) e. B ) )