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	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )