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

Metamath Proof Explorer

Theorem ac5b

Description: Equivalent of Axiom of Choice. (Contributed by NM, 31-Aug-1999)

Ref Expression
Hypothesis ac5b.1 ⊢ A ∈ V
Assertion ac5b ⊢ ∀ x ∈ A x ≠ ∅ → ∃ f f : A ⟶ ⋃ A ∧ ∀ x ∈ A f ⁡ x ∈ x

Proof

Step Hyp Ref Expression
1 ac5b.1 ⊢ A ∈ V
2 1 uniex ⊢ ⋃ A ∈ V
3 numth3 ⊢ ⋃ A ∈ V → ⋃ A ∈ dom ⁡ card
4 2 3 mp1i ⊢ ∀ x ∈ A x ≠ ∅ → ⋃ A ∈ dom ⁡ card
5 neirr ⊢ ¬ ∅ ≠ ∅
6 neeq1 ⊢ x = ∅ → x ≠ ∅ ↔ ∅ ≠ ∅
7 6 rspccv ⊢ ∀ x ∈ A x ≠ ∅ → ∅ ∈ A → ∅ ≠ ∅
8 5 7 mtoi ⊢ ∀ x ∈ A x ≠ ∅ → ¬ ∅ ∈ A
9 ac5num ⊢ ⋃ A ∈ dom ⁡ card ∧ ¬ ∅ ∈ A → ∃ f f : A ⟶ ⋃ A ∧ ∀ x ∈ A f ⁡ x ∈ x
10 4 8 9 syl2anc ⊢ ∀ x ∈ A x ≠ ∅ → ∃ f f : A ⟶ ⋃ A ∧ ∀ x ∈ A f ⁡ x ∈ x