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	syl5bi	⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) ) )
63	62	exlimdv	⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ( ∃ 𝑓 ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) ) )
64	11 63	mpd	⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) )