Metamath Proof Explorer

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 ⊢ φ → F Fn V
gblacfnacd.2 ⊢ φ → ∀ z z ≠ ∅ → F ⁡ z ∈ z
Assertion gblacfnacd ⊢ φ → ∀ x ∃ f f Fn x ∧ ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ z

Proof

Step Hyp Ref Expression
1 gblacfnacd.1 ⊢ φ → F Fn V
2 gblacfnacd.2 ⊢ φ → ∀ z z ≠ ∅ → F ⁡ z ∈ z
3 fnfun ⊢ F Fn V → Fun ⁡ F
4 resfunexg ⊢ Fun ⁡ F ∧ x ∈ V → F ↾ x ∈ V
5 4 elvd ⊢ Fun ⁡ F → F ↾ x ∈ V
6 1 3 5 3syl ⊢ φ → F ↾ x ∈ V
7 ssv ⊢ x ⊆ V
8 fnssres ⊢ F Fn V ∧ x ⊆ V → F ↾ x Fn x
9 1 7 8 sylancl ⊢ φ → F ↾ x Fn x
10 2 19.21bi ⊢ φ → z ≠ ∅ → F ⁡ z ∈ z
11 fvres ⊢ z ∈ x → F ↾ x ⁡ z = F ⁡ z
12 11 eleq1d ⊢ z ∈ x → F ↾ x ⁡ z ∈ z ↔ F ⁡ z ∈ z
13 12 imbi2d ⊢ z ∈ x → z ≠ ∅ → F ↾ x ⁡ z ∈ z ↔ z ≠ ∅ → F ⁡ z ∈ z
14 10 13 syl5ibrcom ⊢ φ → z ∈ x → z ≠ ∅ → F ↾ x ⁡ z ∈ z
15 14 ralrimiv ⊢ φ → ∀ z ∈ x z ≠ ∅ → F ↾ x ⁡ z ∈ z
16 9 15 jca ⊢ φ → F ↾ x Fn x ∧ ∀ z ∈ x z ≠ ∅ → F ↾ x ⁡ z ∈ 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 ∈ z ↔ F ↾ x ⁡ z ∈ z
20 19 imbi2d ⊢ f = F ↾ x → z ≠ ∅ → f ⁡ z ∈ z ↔ z ≠ ∅ → F ↾ x ⁡ z ∈ z
21 20 ralbidv ⊢ f = F ↾ x → ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ z ↔ ∀ z ∈ x z ≠ ∅ → F ↾ x ⁡ z ∈ z
22 17 21 anbi12d ⊢ f = F ↾ x → f Fn x ∧ ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ z ↔ F ↾ x Fn x ∧ ∀ z ∈ x z ≠ ∅ → F ↾ x ⁡ z ∈ z
23 6 16 22 spcedv ⊢ φ → ∃ f f Fn x ∧ ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ z
24 23 alrimiv ⊢ φ → ∀ x ∃ f f Fn x ∧ ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ z