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 ⊢ ( 𝜑 → 𝐴 ∈ 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 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )