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 ( 𝜑𝐴 ∈ Fin )
choicefi.b ( ( 𝜑𝑥𝐴 ) → 𝐵𝑊 )
choicefi.n ( ( 𝜑𝑥𝐴 ) → 𝐵 ≠ ∅ )
Assertion choicefi ( 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )

Proof

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