Theorem gblacfnacd

Description: If F is a global choice function, then the Axiom of Choice (in the form of the right-hand side of dfac4 ) holds. Note that F must be a proper class by fndmexb . This means we cannot show that the existence of a class that behaves as a global choice function is sufficient because we only have existential quantifiers for sets, not (proper) classes. However, if a class variant of exlimiv were available, then it could be used alongside the closed form of this theorem to prove that result. (Contributed by BTernaryTau, 12-Dec-2024)

	Ref	Expression
Hypotheses	gblacfnacd.1	⊢ ( 𝜑 → 𝐹 Fn V )
	gblacfnacd.2	⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
Assertion	gblacfnacd	⊢ ( 𝜑 → ∀ 𝑥 ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gblacfnacd.1	⊢ ( 𝜑 → 𝐹 Fn V )
2		gblacfnacd.2	⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
3		fnfun	⊢ ( 𝐹 Fn V → Fun 𝐹 )
4		resfunexg	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ V ) → ( 𝐹 ↾ 𝑥 ) ∈ V )
5	4	elvd	⊢ ( Fun 𝐹 → ( 𝐹 ↾ 𝑥 ) ∈ V )
6	1 3 5	3syl	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑥 ) ∈ V )
7		ssv	⊢ 𝑥 ⊆ V
8		fnssres	⊢ ( ( 𝐹 Fn V ∧ 𝑥 ⊆ V ) → ( 𝐹 ↾ 𝑥 ) Fn 𝑥 )
9	1 7 8	sylancl	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑥 ) Fn 𝑥 )
10	2	19.21bi	⊢ ( 𝜑 → ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
11		fvres	⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
12	11	eleq1d	⊢ ( 𝑧 ∈ 𝑥 → ( ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
13	12	imbi2d	⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑧 ≠ ∅ → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ) )
14	10 13	syl5ibrcom	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑥 → ( 𝑧 ≠ ∅ → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
15	14	ralrimiv	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑧 ) ∈ 𝑧 ) )
16	9 15	jca	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝑥 ) Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
17		fneq1	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( 𝑓 Fn 𝑥 ↔ ( 𝐹 ↾ 𝑥 ) Fn 𝑥 ) )
18		fveq1	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( 𝑓 ‘ 𝑧 ) = ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑧 ) )
19	18	eleq1d	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑧 ) ∈ 𝑧 ) )
20	19	imbi2d	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
21	20	ralbidv	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
22	17 21	anbi12d	⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ↔ ( ( 𝐹 ↾ 𝑥 ) Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑧 ) ∈ 𝑧 ) ) ) )
23	6 16 22	spcedv	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
24	23	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )