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 φAFin
choicefi.b φxABW
choicefi.n φxAB
Assertion choicefi φffFnAxAfxB

Proof

Step Hyp Ref Expression
1 choicefi.a φAFin
2 choicefi.b φxABW
3 choicefi.n φxAB
4 mptfi AFinxABFin
5 1 4 syl φxABFin
6 rnfi xABFinranxABFin
7 5 6 syl φranxABFin
8 fnchoice ranxABFinggFnranxAByranxABygyy
9 7 8 syl φggFnranxAByranxABygyy
10 simpl φgFnranxAByranxABygyyφ
11 simprl φgFnranxAByranxABygyygFnranxAB
12 nfv yφ
13 nfra1 yyranxABygyy
14 12 13 nfan yφyranxABygyy
15 rspa yranxABygyyyranxABygyy
16 15 adantll φyranxABygyyyranxABygyy
17 vex yV
18 eqid xAB=xAB
19 18 elrnmpt yVyranxABxAy=B
20 17 19 ax-mp yranxABxAy=B
21 20 biimpi yranxABxAy=B
22 21 adantl φyranxABxAy=B
23 simp3 φxAy=By=B
24 3 3adant3 φxAy=BB
25 23 24 eqnetrd φxAy=By
26 25 3exp φxAy=By
27 26 rexlimdv φxAy=By
28 27 adantr φyranxABxAy=By
29 22 28 mpd φyranxABy
30 29 adantlr φyranxABygyyyranxABy
31 id ygyyygyy
32 31 imp ygyyygyy
33 16 30 32 syl2anc φyranxABygyyyranxABgyy
34 33 ex φyranxABygyyyranxABgyy
35 14 34 ralrimi φyranxABygyyyranxABgyy
36 rsp yranxABgyyyranxABgyy
37 35 36 syl φyranxABygyyyranxABgyy
38 14 37 ralrimi φyranxABygyyyranxABgyy
39 38 adantrl φgFnranxAByranxABygyyyranxABgyy
40 vex gV
41 40 a1i φgV
42 1 mptexd φxABV
43 coexg gVxABVgxABV
44 41 42 43 syl2anc φgxABV
45 44 3ad2ant1 φgFnranxAByranxABgyygxABV
46 simpr φgFnranxABgFnranxAB
47 2 ralrimiva φxABW
48 18 fnmpt xABWxABFnA
49 47 48 syl φxABFnA
50 49 adantr φgFnranxABxABFnA
51 ssidd φgFnranxABranxABranxAB
52 fnco gFnranxABxABFnAranxABranxABgxABFnA
53 46 50 51 52 syl3anc φgFnranxABgxABFnA
54 53 3adant3 φgFnranxAByranxABgyygxABFnA
55 nfv xφ
56 nfcv _xg
57 nfmpt1 _xxAB
58 57 nfrn _xranxAB
59 56 58 nffn xgFnranxAB
60 nfv xgyy
61 58 60 nfralw xyranxABgyy
62 55 59 61 nf3an xφgFnranxAByranxABgyy
63 funmpt FunxAB
64 63 a1i φxAFunxAB
65 simpr φxAxA
66 18 2 dmmptd φdomxAB=A
67 66 eqcomd φA=domxAB
68 67 adantr φxAA=domxAB
69 65 68 eleqtrd φxAxdomxAB
70 fvco FunxABxdomxABgxABx=gxABx
71 64 69 70 syl2anc φxAgxABx=gxABx
72 18 fvmpt2 xABWxABx=B
73 65 2 72 syl2anc φxAxABx=B
74 73 fveq2d φxAgxABx=gB
75 71 74 eqtrd φxAgxABx=gB
76 75 3ad2antl1 φgFnranxAByranxABgyyxAgxABx=gB
77 18 elrnmpt1 xABWBranxAB
78 65 2 77 syl2anc φxABranxAB
79 78 3ad2antl1 φgFnranxAByranxABgyyxABranxAB
80 simpl3 φgFnranxAByranxABgyyxAyranxABgyy
81 fveq2 y=Bgy=gB
82 id y=By=B
83 81 82 eleq12d y=BgyygBB
84 83 rspcva BranxAByranxABgyygBB
85 79 80 84 syl2anc φgFnranxAByranxABgyyxAgBB
86 76 85 eqeltrd φgFnranxAByranxABgyyxAgxABxB
87 86 ex φgFnranxAByranxABgyyxAgxABxB
88 62 87 ralrimi φgFnranxAByranxABgyyxAgxABxB
89 54 88 jca φgFnranxAByranxABgyygxABFnAxAgxABxB
90 fneq1 f=gxABfFnAgxABFnA
91 nfcv _xf
92 56 57 nfco _xgxAB
93 91 92 nfeq xf=gxAB
94 fveq1 f=gxABfx=gxABx
95 94 eleq1d f=gxABfxBgxABxB
96 93 95 ralbid f=gxABxAfxBxAgxABxB
97 90 96 anbi12d f=gxABfFnAxAfxBgxABFnAxAgxABxB
98 97 spcegv gxABVgxABFnAxAgxABxBffFnAxAfxB
99 45 89 98 sylc φgFnranxAByranxABgyyffFnAxAfxB
100 10 11 39 99 syl3anc φgFnranxAByranxABygyyffFnAxAfxB
101 100 ex φgFnranxAByranxABygyyffFnAxAfxB
102 101 exlimdv φggFnranxAByranxABygyyffFnAxAfxB
103 9 102 mpd φffFnAxAfxB