Metamath Proof Explorer


Theorem ac5b

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

Ref Expression
Hypothesis ac5b.1 𝐴 ∈ V
Assertion ac5b ( ∀ 𝑥𝐴 𝑥 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝐴 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 ac5b.1 𝐴 ∈ V
2 1 uniex 𝐴 ∈ V
3 numth3 ( 𝐴 ∈ V → 𝐴 ∈ dom card )
4 2 3 mp1i ( ∀ 𝑥𝐴 𝑥 ≠ ∅ → 𝐴 ∈ dom card )
5 neirr ¬ ∅ ≠ ∅
6 neeq1 ( 𝑥 = ∅ → ( 𝑥 ≠ ∅ ↔ ∅ ≠ ∅ ) )
7 6 rspccv ( ∀ 𝑥𝐴 𝑥 ≠ ∅ → ( ∅ ∈ 𝐴 → ∅ ≠ ∅ ) )
8 5 7 mtoi ( ∀ 𝑥𝐴 𝑥 ≠ ∅ → ¬ ∅ ∈ 𝐴 )
9 ac5num ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 : 𝐴 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝑥 ) )
10 4 8 9 syl2anc ( ∀ 𝑥𝐴 𝑥 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝐴 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝑥 ) )