This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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. (Contributed by NM, 18-Oct-1999) (Revised by Mario Carneiro, 27-Aug-2015)

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

Proof

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