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