Metamath Proof Explorer

Theorem ac6

Description: Equivalent of Axiom of Choice. This is useful for proving that there exists, for example, a sequence mapping natural numbers to members of a larger set B , where ph depends on x (the natural number) and y (to specify a member of B ). A stronger version of this theorem, ac6s , allows B to be a proper class. Unlike ac6sg , which allows B to be a proper class and so uses the Collection principle bnd2 , this needs neither ax-reg nor ax-inf2 . (Contributed by NM, 18-Oct-1999) (Revised by Mario Carneiro, 27-Aug-2015) Replace hypotheses with antecedents. (Revised by Timothy J. O'Malley, 15-Oct-2026)

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

Proof

Step Hyp Ref Expression
1 ac6.1 ⊢ y = f ⁡ x → φ ↔ ψ
2 ssrab2 ⊢ y ∈ B | φ ⊆ B
3 2 rgenw ⊢ ∀ x ∈ A y ∈ B | φ ⊆ B
4 iunss ⊢ ⋃ x ∈ A y ∈ B | φ ⊆ B ↔ ∀ x ∈ A y ∈ B | φ ⊆ B
5 3 4 mpbir ⊢ ⋃ x ∈ A y ∈ B | φ ⊆ B
6 ssexg ⊢ ⋃ x ∈ A y ∈ B | φ ⊆ B ∧ B ∈ W → ⋃ x ∈ A y ∈ B | φ ∈ V
7 5 6 mpan ⊢ B ∈ W → ⋃ x ∈ A y ∈ B | φ ∈ V
8 numth3 ⊢ ⋃ x ∈ A y ∈ B | φ ∈ V → ⋃ x ∈ A y ∈ B | φ ∈ dom ⁡ card
9 7 8 syl ⊢ B ∈ W → ⋃ x ∈ A y ∈ B | φ ∈ dom ⁡ card
10 1 ac6num ⊢ A ∈ V ∧ ⋃ x ∈ A y ∈ B | φ ∈ dom ⁡ card ∧ ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ
11 9 10 syl3an2 ⊢ A ∈ V ∧ B ∈ W ∧ ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ