Metamath Proof Explorer

Theorem ac6s

Description: Equivalent of Axiom of Choice. Using the Boundedness Axiom bnd2 , we derive this strong version of ac6 that doesn't require B to be a set. (Contributed by NM, 4-Feb-2004)

Ref Expression
Hypotheses ac6s.1 ⊢ A ∈ V
ac6s.2 ⊢ y = f ⁡ x → φ ↔ ψ
Assertion ac6s ⊢ ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 ac6s.1 ⊢ A ∈ V
2 ac6s.2 ⊢ y = f ⁡ x → φ ↔ ψ
3 1 bnd2 ⊢ ∀ x ∈ A ∃ y ∈ B φ → ∃ z z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z φ
4 vex ⊢ z ∈ V
5 2 ac6 ⊢ A ∈ V ∧ z ∈ V ∧ ∀ x ∈ A ∃ y ∈ z φ → ∃ f f : A ⟶ z ∧ ∀ x ∈ A ψ
6 1 4 5 mp3an12 ⊢ ∀ x ∈ A ∃ y ∈ z φ → ∃ f f : A ⟶ z ∧ ∀ x ∈ A ψ
7 6 anim2i ⊢ z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z φ → z ⊆ B ∧ ∃ f f : A ⟶ z ∧ ∀ x ∈ A ψ
8 7 eximi ⊢ ∃ z z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z φ → ∃ z z ⊆ B ∧ ∃ f f : A ⟶ z ∧ ∀ x ∈ A ψ
9 fss ⊢ f : A ⟶ z ∧ z ⊆ B → f : A ⟶ B
10 9 expcom ⊢ z ⊆ B → f : A ⟶ z → f : A ⟶ B
11 10 anim1d ⊢ z ⊆ B → f : A ⟶ z ∧ ∀ x ∈ A ψ → f : A ⟶ B ∧ ∀ x ∈ A ψ
12 11 eximdv ⊢ z ⊆ B → ∃ f f : A ⟶ z ∧ ∀ x ∈ A ψ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ
13 12 imp ⊢ z ⊆ B ∧ ∃ f f : A ⟶ z ∧ ∀ x ∈ A ψ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ
14 13 exlimiv ⊢ ∃ z z ⊆ B ∧ ∃ f f : A ⟶ z ∧ ∀ x ∈ A ψ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ
15 3 8 14 3syl ⊢ ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ