Description: Equivalent of Axiom of Choice. (Contributed by NM, 31-Aug-1999)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ac5b.1 | ⊢ 𝐴 ∈ V | |
Assertion | ac5b | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
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 | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |