Metamath Proof Explorer

Theorem choicefi

Description: For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses choicefi.a 
|- ( ph -> A e. Fin )
choicefi.b 
|- ( ( ph /\ x e. A ) -> B e. W )
choicefi.n 
|- ( ( ph /\ x e. A ) -> B =/= (/) )
Assertion choicefi 
|- ( ph -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )

Proof

Step Hyp Ref Expression
1 choicefi.a 
 |-  ( ph -> A e. Fin )
2 choicefi.b 
 |-  ( ( ph /\ x e. A ) -> B e. W )
3 choicefi.n 
 |-  ( ( ph /\ x e. A ) -> B =/= (/) )
4 mptfi 
 |-  ( A e. Fin -> ( x e. A |-> B ) e. Fin )
5 rnfi 
 |-  ( ( x e. A |-> B ) e. Fin -> ran ( x e. A |-> B ) e. Fin )
6 fnchoice 
 |-  ( ran ( x e. A |-> B ) e. Fin -> E. g ( g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) )
7 1 4 5 6 4syl 
 |-  ( ph -> E. g ( g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) )
8 simpl 
 |-  ( ( ph /\ ( g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) ) -> ph )
9 simprl 
 |-  ( ( ph /\ ( g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) ) -> g Fn ran ( x e. A |-> B ) )
10 nfv 
 |-  F/ y ph
11 nfra1 
 |-  F/ y A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y )
12 10 11 nfan 
 |-  F/ y ( ph /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) )
13 rspa 
 |-  ( ( A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) /\ y e. ran ( x e. A |-> B ) ) -> ( y =/= (/) -> ( g ` y ) e. y ) )
14 13 adantll 
 |-  ( ( ( ph /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) /\ y e. ran ( x e. A |-> B ) ) -> ( y =/= (/) -> ( g ` y ) e. y ) )
15 vex 
 |-  y e. _V
16 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
17 16 elrnmpt 
 |-  ( y e. _V -> ( y e. ran ( x e. A |-> B ) <-> E. x e. A y = B ) )
18 15 17 ax-mp 
 |-  ( y e. ran ( x e. A |-> B ) <-> E. x e. A y = B )
19 18 bilani 
 |-  ( ( ph /\ y e. ran ( x e. A |-> B ) ) -> E. x e. A y = B )
20 simp3 
 |-  ( ( ph /\ x e. A /\ y = B ) -> y = B )
21 3 3adant3 
 |-  ( ( ph /\ x e. A /\ y = B ) -> B =/= (/) )
22 20 21 eqnetrd 
 |-  ( ( ph /\ x e. A /\ y = B ) -> y =/= (/) )
23 22 3exp 
 |-  ( ph -> ( x e. A -> ( y = B -> y =/= (/) ) ) )
24 23 rexlimdv 
 |-  ( ph -> ( E. x e. A y = B -> y =/= (/) ) )
25 24 adantr 
 |-  ( ( ph /\ y e. ran ( x e. A |-> B ) ) -> ( E. x e. A y = B -> y =/= (/) ) )
26 19 25 mpd 
 |-  ( ( ph /\ y e. ran ( x e. A |-> B ) ) -> y =/= (/) )
27 26 adantlr 
 |-  ( ( ( ph /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) /\ y e. ran ( x e. A |-> B ) ) -> y =/= (/) )
28 id 
 |-  ( ( y =/= (/) -> ( g ` y ) e. y ) -> ( y =/= (/) -> ( g ` y ) e. y ) )
29 28 imp 
 |-  ( ( ( y =/= (/) -> ( g ` y ) e. y ) /\ y =/= (/) ) -> ( g ` y ) e. y )
30 14 27 29 syl2anc 
 |-  ( ( ( ph /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) /\ y e. ran ( x e. A |-> B ) ) -> ( g ` y ) e. y )
31 30 ex 
 |-  ( ( ph /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) -> ( y e. ran ( x e. A |-> B ) -> ( g ` y ) e. y ) )
32 12 31 ralrimi 
 |-  ( ( ph /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) -> A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y )
33 rsp 
 |-  ( A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y -> ( y e. ran ( x e. A |-> B ) -> ( g ` y ) e. y ) )
34 32 33 syl 
 |-  ( ( ph /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) -> ( y e. ran ( x e. A |-> B ) -> ( g ` y ) e. y ) )
35 12 34 ralrimi 
 |-  ( ( ph /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) -> A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y )
36 35 adantrl 
 |-  ( ( ph /\ ( g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) ) -> A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y )
37 vex 
 |-  g e. _V
38 37 a1i 
 |-  ( ph -> g e. _V )
39 1 mptexd 
 |-  ( ph -> ( x e. A |-> B ) e. _V )
40 coexg 
 |-  ( ( g e. _V /\ ( x e. A |-> B ) e. _V ) -> ( g o. ( x e. A |-> B ) ) e. _V )
41 38 39 40 syl2anc 
 |-  ( ph -> ( g o. ( x e. A |-> B ) ) e. _V )
42 41 3ad2ant1 
 |-  ( ( ph /\ g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y ) -> ( g o. ( x e. A |-> B ) ) e. _V )
43 simpr 
 |-  ( ( ph /\ g Fn ran ( x e. A |-> B ) ) -> g Fn ran ( x e. A |-> B ) )
44 2 ralrimiva 
 |-  ( ph -> A. x e. A B e. W )
45 16 fnmpt 
 |-  ( A. x e. A B e. W -> ( x e. A |-> B ) Fn A )
46 44 45 syl 
 |-  ( ph -> ( x e. A |-> B ) Fn A )
47 46 adantr 
 |-  ( ( ph /\ g Fn ran ( x e. A |-> B ) ) -> ( x e. A |-> B ) Fn A )
48 ssidd 
 |-  ( ( ph /\ g Fn ran ( x e. A |-> B ) ) -> ran ( x e. A |-> B ) C_ ran ( x e. A |-> B ) )
49 fnco 
 |-  ( ( g Fn ran ( x e. A |-> B ) /\ ( x e. A |-> B ) Fn A /\ ran ( x e. A |-> B ) C_ ran ( x e. A |-> B ) ) -> ( g o. ( x e. A |-> B ) ) Fn A )
50 43 47 48 49 syl3anc 
 |-  ( ( ph /\ g Fn ran ( x e. A |-> B ) ) -> ( g o. ( x e. A |-> B ) ) Fn A )
51 50 3adant3 
 |-  ( ( ph /\ g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y ) -> ( g o. ( x e. A |-> B ) ) Fn A )
52 nfv 
 |-  F/ x ph
53 nfcv 
 |-  F/_ x g
54 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
55 54 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
56 53 55 nffn 
 |-  F/ x g Fn ran ( x e. A |-> B )
57 nfv 
 |-  F/ x ( g ` y ) e. y
58 55 57 nfralw 
 |-  F/ x A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y
59 52 56 58 nf3an 
 |-  F/ x ( ph /\ g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y )
60 funmpt 
 |-  Fun ( x e. A |-> B )
61 60 a1i 
 |-  ( ( ph /\ x e. A ) -> Fun ( x e. A |-> B ) )
62 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
63 16 2 dmmptd 
 |-  ( ph -> dom ( x e. A |-> B ) = A )
64 63 eqcomd 
 |-  ( ph -> A = dom ( x e. A |-> B ) )
65 64 adantr 
 |-  ( ( ph /\ x e. A ) -> A = dom ( x e. A |-> B ) )
66 62 65 eleqtrd 
 |-  ( ( ph /\ x e. A ) -> x e. dom ( x e. A |-> B ) )
67 fvco 
 |-  ( ( Fun ( x e. A |-> B ) /\ x e. dom ( x e. A |-> B ) ) -> ( ( g o. ( x e. A |-> B ) ) ` x ) = ( g ` ( ( x e. A |-> B ) ` x ) ) )
68 61 66 67 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( g o. ( x e. A |-> B ) ) ` x ) = ( g ` ( ( x e. A |-> B ) ` x ) ) )
69 16 fvmpt2 
 |-  ( ( x e. A /\ B e. W ) -> ( ( x e. A |-> B ) ` x ) = B )
70 62 2 69 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
71 70 fveq2d 
 |-  ( ( ph /\ x e. A ) -> ( g ` ( ( x e. A |-> B ) ` x ) ) = ( g ` B ) )
72 68 71 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( ( g o. ( x e. A |-> B ) ) ` x ) = ( g ` B ) )
73 72 3ad2antl1 
 |-  ( ( ( ph /\ g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y ) /\ x e. A ) -> ( ( g o. ( x e. A |-> B ) ) ` x ) = ( g ` B ) )
74 16 elrnmpt1 
 |-  ( ( x e. A /\ B e. W ) -> B e. ran ( x e. A |-> B ) )
75 62 2 74 syl2anc 
 |-  ( ( ph /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
76 75 3ad2antl1 
 |-  ( ( ( ph /\ g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y ) /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
77 simpl3 
 |-  ( ( ( ph /\ g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y ) /\ x e. A ) -> A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y )
78 fveq2 
 |-  ( y = B -> ( g ` y ) = ( g ` B ) )
79 id 
 |-  ( y = B -> y = B )
80 78 79 eleq12d 
 |-  ( y = B -> ( ( g ` y ) e. y <-> ( g ` B ) e. B ) )
81 80 rspcva 
 |-  ( ( B e. ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y ) -> ( g ` B ) e. B )
82 76 77 81 syl2anc 
 |-  ( ( ( ph /\ g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y ) /\ x e. A ) -> ( g ` B ) e. B )
83 73 82 eqeltrd 
 |-  ( ( ( ph /\ g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y ) /\ x e. A ) -> ( ( g o. ( x e. A |-> B ) ) ` x ) e. B )
84 83 ex 
 |-  ( ( ph /\ g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y ) -> ( x e. A -> ( ( g o. ( x e. A |-> B ) ) ` x ) e. B ) )
85 59 84 ralrimi 
 |-  ( ( ph /\ g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y ) -> A. x e. A ( ( g o. ( x e. A |-> B ) ) ` x ) e. B )
86 51 85 jca 
 |-  ( ( ph /\ g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y ) -> ( ( g o. ( x e. A |-> B ) ) Fn A /\ A. x e. A ( ( g o. ( x e. A |-> B ) ) ` x ) e. B ) )
87 fneq1 
 |-  ( f = ( g o. ( x e. A |-> B ) ) -> ( f Fn A <-> ( g o. ( x e. A |-> B ) ) Fn A ) )
88 nfcv 
 |-  F/_ x f
89 53 54 nfco 
 |-  F/_ x ( g o. ( x e. A |-> B ) )
90 88 89 nfeq 
 |-  F/ x f = ( g o. ( x e. A |-> B ) )
91 fveq1 
 |-  ( f = ( g o. ( x e. A |-> B ) ) -> ( f ` x ) = ( ( g o. ( x e. A |-> B ) ) ` x ) )
92 91 eleq1d 
 |-  ( f = ( g o. ( x e. A |-> B ) ) -> ( ( f ` x ) e. B <-> ( ( g o. ( x e. A |-> B ) ) ` x ) e. B ) )
93 90 92 ralbid 
 |-  ( f = ( g o. ( x e. A |-> B ) ) -> ( A. x e. A ( f ` x ) e. B <-> A. x e. A ( ( g o. ( x e. A |-> B ) ) ` x ) e. B ) )
94 87 93 anbi12d 
 |-  ( f = ( g o. ( x e. A |-> B ) ) -> ( ( f Fn A /\ A. x e. A ( f ` x ) e. B ) <-> ( ( g o. ( x e. A |-> B ) ) Fn A /\ A. x e. A ( ( g o. ( x e. A |-> B ) ) ` x ) e. B ) ) )
95 94 spcegv 
 |-  ( ( g o. ( x e. A |-> B ) ) e. _V -> ( ( ( g o. ( x e. A |-> B ) ) Fn A /\ A. x e. A ( ( g o. ( x e. A |-> B ) ) ` x ) e. B ) -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) ) )
96 42 86 95 sylc 
 |-  ( ( ph /\ g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( g ` y ) e. y ) -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
97 8 9 36 96 syl3anc 
 |-  ( ( ph /\ ( g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) ) -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
98 97 ex 
 |-  ( ph -> ( ( g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) ) )
99 98 exlimdv 
 |-  ( ph -> ( E. g ( g Fn ran ( x e. A |-> B ) /\ A. y e. ran ( x e. A |-> B ) ( y =/= (/) -> ( g ` y ) e. y ) ) -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) ) )
100 7 99 mpd 
 |-  ( ph -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )