Metamath Proof Explorer

Theorem gblacfnacd

Description: If G is a global choice function, then the Axiom of Choice (in the form of the right-hand side of dfac4 ) holds. Note that G 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 ⊢ φ → G Fn V
gblacfnacd.2 ⊢ φ → ∀ z z ≠ ∅ → G ⁡ z ∈ z
Assertion gblacfnacd ⊢ φ → ∀ x ∃ f f Fn x ∧ ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ z

Proof

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