This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem acni2

Description: The property of being a choice set of length A . (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acni2 ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ ( 𝐵 ∈ ( 𝒫 𝑋 ∖ { ∅ } ) ↔ ( 𝐵 ∈ 𝒫 𝑋 ∧ 𝐵 ≠ ∅ ) )
2 elpw2g ⊢ ( 𝑋 ∈ AC 𝐴 → ( 𝐵 ∈ 𝒫 𝑋 ↔ 𝐵 ⊆ 𝑋 ) )
3 2 anbi1d ⊢ ( 𝑋 ∈ AC 𝐴 → ( ( 𝐵 ∈ 𝒫 𝑋 ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) )
4 1 3 bitrid ⊢ ( 𝑋 ∈ AC 𝐴 → ( 𝐵 ∈ ( 𝒫 𝑋 ∖ { ∅ } ) ↔ ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) )
5 4 ralbidv ⊢ ( 𝑋 ∈ AC 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝒫 𝑋 ∖ { ∅ } ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) )
6 5 biimpar ⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝒫 𝑋 ∖ { ∅ } ) )
7 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
8 7 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝒫 𝑋 ∖ { ∅ } ) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 𝒫 𝑋 ∖ { ∅ } ) )
9 6 8 sylib ⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 𝒫 𝑋 ∖ { ∅ } ) )
10 acni ⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 𝒫 𝑋 ∖ { ∅ } ) ) → ∃ 𝑓 ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) )
11 9 10 syldan ⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑓 ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) )
12 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
13 12 nfel2 ⊢ Ⅎ 𝑥 ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
14 nfv ⊢ Ⅎ 𝑦 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 )
15 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑥 ) )
16 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
17 15 16 eleq12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
18 13 14 17 cbvralw ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
19 simplr ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) )
20 simplr ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ⊆ 𝑋 ) → 𝑥 ∈ 𝐴 )
21 simpll ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ⊆ 𝑋 ) → 𝑋 ∈ AC 𝐴 )
22 simpr ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ⊆ 𝑋 ) → 𝐵 ⊆ 𝑋 )
23 21 22 ssexd ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ⊆ 𝑋 ) → 𝐵 ∈ V )
24 7 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
25 20 23 24 syl2anc ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
26 25 eleq2d ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ⊆ 𝑋 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
27 26 ex ⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ⊆ 𝑋 → ( ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) )
28 27 adantrd ⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) )
29 28 ralimdva ⊢ ( 𝑋 ∈ AC 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) )
30 29 imp ⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
31 ralbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
32 30 31 syl ⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
33 32 biimpa ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
34 ssel ⊢ ( 𝐵 ⊆ 𝑋 → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑋 ) )
35 34 adantr ⊢ ( ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑋 ) )
36 35 ral2imi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑋 ) )
37 19 33 36 sylc ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑋 )
38 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑦 ) )
39 38 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑋 ↔ ( 𝑓 ‘ 𝑦 ) ∈ 𝑋 ) )
40 39 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑋 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝑋 )
41 37 40 sylan ⊢ ( ( ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝑋 )
42 41 fmpttd ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) → ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : 𝐴 ⟶ 𝑋 )
43 simpll ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) → 𝑋 ∈ AC 𝐴 )
44 acnrcl ⊢ ( 𝑋 ∈ AC 𝐴 → 𝐴 ∈ V )
45 43 44 syl ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) → 𝐴 ∈ V )
46 fex2 ⊢ ( ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : 𝐴 ⟶ 𝑋 ∧ 𝐴 ∈ V ∧ 𝑋 ∈ AC 𝐴 ) → ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ∈ V )
47 42 45 43 46 syl3anc ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) → ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ∈ V )
48 eqid ⊢ ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) )
49 fvex ⊢ ( 𝑓 ‘ 𝑥 ) ∈ V
50 15 48 49 fvmpt ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
51 50 eleq1d ⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
52 51 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
53 33 52 sylibr ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝐵 )
54 42 53 jca ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) → ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝐵 ) )
55 feq1 ⊢ ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) → ( 𝑔 : 𝐴 ⟶ 𝑋 ↔ ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : 𝐴 ⟶ 𝑋 ) )
56 fveq1 ⊢ ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) → ( 𝑔 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ‘ 𝑥 ) )
57 56 eleq1d ⊢ ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) → ( ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ↔ ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝐵 ) )
58 57 ralbidv ⊢ ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝐵 ) )
59 55 58 anbi12d ⊢ ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) → ( ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) ↔ ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝐵 ) ) )
60 47 54 59 spcedv ⊢ ( ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) )
61 60 ex ⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) ) )
62 18 61 biimtrid ⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) ) )
63 62 exlimdv ⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ( ∃ 𝑓 ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) ) )
64 11 63 mpd ⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) )