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 φ A Fin
choicefi.b φ x A B W
choicefi.n φ x A B
Assertion choicefi φ f f Fn A x A f x B

Proof

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