# 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 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
choicefi.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {W}$
choicefi.n ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\ne \varnothing$
Assertion choicefi ${⊢}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)$

### Proof

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