This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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