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 bilani ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
20 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
21 3 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐵 ≠ ∅ )
22 20 21 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑦 ≠ ∅ )
23 22 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑦 = 𝐵 → 𝑦 ≠ ∅ ) ) )
24 23 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 → 𝑦 ≠ ∅ ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 → 𝑦 ≠ ∅ ) )
26 19 25 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑦 ≠ ∅ )
27 26 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑦 ≠ ∅ )
28 id ⊢ ( ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) )
29 28 imp ⊢ ( ( ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑦 ≠ ∅ ) → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 )
30 14 27 29 syl2anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 )
31 30 ex ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) → ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) )
32 12 31 ralrimi ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) → ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 )
33 rsp ⊢ ( ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 → ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) )
34 32 33 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) → ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) )
35 12 34 ralrimi ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) → ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 )
36 35 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) ) → ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 )
37 vex ⊢ 𝑔 ∈ V
38 37 a1i ⊢ ( 𝜑 → 𝑔 ∈ V )
39 1 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
40 coexg ⊢ ( ( 𝑔 ∈ V ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) → ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ V )
41 38 39 40 syl2anc ⊢ ( 𝜑 → ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ V )
42 41 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ V )
43 simpr ⊢ ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
44 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 )
45 16 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
46 44 45 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
48 ssidd ⊢ ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
49 fnco ⊢ ( ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) Fn 𝐴 )
50 43 47 48 49 syl3anc ⊢ ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) Fn 𝐴 )
51 50 3adant3 ⊢ ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) Fn 𝐴 )
52 nfv ⊢ Ⅎ 𝑥 𝜑
53 nfcv ⊢ Ⅎ 𝑥 𝑔
54 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
55 54 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
56 53 55 nffn ⊢ Ⅎ 𝑥 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
57 nfv ⊢ Ⅎ 𝑥 ( 𝑔 ‘ 𝑦 ) ∈ 𝑦
58 55 57 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦
59 52 56 58 nf3an ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 )
60 funmpt ⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
61 60 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
62 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
63 16 2 dmmptd ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
64 63 eqcomd ⊢ ( 𝜑 → 𝐴 = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
66 62 65 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
67 fvco ⊢ ( ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ 𝑥 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) = ( 𝑔 ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
68 61 66 67 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) = ( 𝑔 ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
69 16 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
70 62 2 69 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
71 70 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) = ( 𝑔 ‘ 𝐵 ) )
72 68 71 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) = ( 𝑔 ‘ 𝐵 ) )
73 72 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) = ( 𝑔 ‘ 𝐵 ) )
74 16 elrnmpt1 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
75 62 2 74 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
76 75 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
77 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 )
78 fveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑔 ‘ 𝑦 ) = ( 𝑔 ‘ 𝐵 ) )
79 id ⊢ ( 𝑦 = 𝐵 → 𝑦 = 𝐵 )
80 78 79 eleq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝑔 ‘ 𝐵 ) ∈ 𝐵 ) )
81 80 rspcva ⊢ ( ( 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( 𝑔 ‘ 𝐵 ) ∈ 𝐵 )
82 76 77 81 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝐵 ) ∈ 𝐵 )
83 73 82 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) ∈ 𝐵 )
84 83 ex ⊢ ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) ∈ 𝐵 ) )
85 59 84 ralrimi ⊢ ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) ∈ 𝐵 )
86 51 85 jca ⊢ ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) ∈ 𝐵 ) )
87 fneq1 ⊢ ( 𝑓 = ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( 𝑓 Fn 𝐴 ↔ ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) Fn 𝐴 ) )
88 nfcv ⊢ Ⅎ 𝑥 𝑓
89 53 54 nfco ⊢ Ⅎ 𝑥 ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
90 88 89 nfeq ⊢ Ⅎ 𝑥 𝑓 = ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
91 fveq1 ⊢ ( 𝑓 = ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( 𝑓 ‘ 𝑥 ) = ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) )
92 91 eleq1d ⊢ ( 𝑓 = ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ↔ ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) ∈ 𝐵 ) )
93 90 92 ralbid ⊢ ( 𝑓 = ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) ∈ 𝐵 ) )
94 87 93 anbi12d ⊢ ( 𝑓 = ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ↔ ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) ∈ 𝐵 ) ) )
95 94 spcegv ⊢ ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ V → ( ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑔 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ‘ 𝑥 ) ∈ 𝐵 ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) )
96 42 86 95 sylc ⊢ ( ( 𝜑 ∧ 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
97 8 9 36 96 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
98 97 ex ⊢ ( 𝜑 → ( ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) )
99 98 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑔 ( 𝑔 Fn ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) )
100 7 99 mpd ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )