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