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	|- ( ph -> F Fn _V )
	gblacfnacd.2	|- ( ph -> A. z ( z =/= (/) -> ( F ` z ) e. z ) )
Assertion	gblacfnacd	|- ( ph -> A. x E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) )

Proof

Step	Hyp	Ref	Expression
1		gblacfnacd.1	|- ( ph -> F Fn _V )
2		gblacfnacd.2	|- ( ph -> A. z ( z =/= (/) -> ( F ` z ) e. z ) )
3		fnfun	|- ( F Fn _V -> Fun F )
4		resfunexg	|- ( ( Fun F /\ x e. _V ) -> ( F |` x ) e. _V )
5	4	elvd	|- ( Fun F -> ( F |` x ) e. _V )
6	1 3 5	3syl	|- ( ph -> ( F |` x ) e. _V )
7		ssv	|- x C_ _V
8		fnssres	|- ( ( F Fn _V /\ x C_ _V ) -> ( F |` x ) Fn x )
9	1 7 8	sylancl	|- ( ph -> ( F |` x ) Fn x )
10	2	19.21bi	|- ( ph -> ( z =/= (/) -> ( F ` z ) e. z ) )
11		fvres	|- ( z e. x -> ( ( F |` x ) ` z ) = ( F ` z ) )
12	11	eleq1d	|- ( z e. x -> ( ( ( F |` x ) ` z ) e. z <-> ( F ` z ) e. z ) )
13	12	imbi2d	|- ( z e. x -> ( ( z =/= (/) -> ( ( F |` x ) ` z ) e. z ) <-> ( z =/= (/) -> ( F ` z ) e. z ) ) )
14	10 13	syl5ibrcom	|- ( ph -> ( z e. x -> ( z =/= (/) -> ( ( F |` x ) ` z ) e. z ) ) )
15	14	ralrimiv	|- ( ph -> A. z e. x ( z =/= (/) -> ( ( F |` x ) ` z ) e. z ) )
16	9 15	jca	|- ( ph -> ( ( F |` x ) Fn x /\ A. z e. x ( z =/= (/) -> ( ( F |` x ) ` z ) e. z ) ) )
17		fneq1	|- ( f = ( F |` x ) -> ( f Fn x <-> ( F |` x ) Fn x ) )
18		fveq1	|- ( f = ( F |` x ) -> ( f ` z ) = ( ( F |` x ) ` z ) )
19	18	eleq1d	|- ( f = ( F |` x ) -> ( ( f ` z ) e. z <-> ( ( F |` x ) ` z ) e. z ) )
20	19	imbi2d	|- ( f = ( F |` x ) -> ( ( z =/= (/) -> ( f ` z ) e. z ) <-> ( z =/= (/) -> ( ( F |` x ) ` z ) e. z ) ) )
21	20	ralbidv	|- ( f = ( F |` x ) -> ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) <-> A. z e. x ( z =/= (/) -> ( ( F |` x ) ` z ) e. z ) ) )
22	17 21	anbi12d	|- ( f = ( F |` x ) -> ( ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) <-> ( ( F |` x ) Fn x /\ A. z e. x ( z =/= (/) -> ( ( F |` x ) ` z ) e. z ) ) ) )
23	6 16 22	spcedv	|- ( ph -> E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) )
24	23	alrimiv	|- ( ph -> A. x E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) )