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

Metamath Proof Explorer

Theorem ac5

Description: An Axiom of Choice equivalent: there exists a function f (called a choice function) with domain A that maps each nonempty member of the domain to an element of that member. Axiom AC of BellMachover p. 488. Note that the assertion that f be a function is not necessary; see ac4 . (Contributed by NM, 29-Aug-1999)

Ref Expression
Hypothesis ac5.1 ⊢ 𝐴 ∈ V
Assertion ac5 ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 ac5.1 ⊢ 𝐴 ∈ V
2 fneq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑓 Fn 𝑦 ↔ 𝑓 Fn 𝐴 ) )
3 raleq ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) )
4 2 3 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) )
5 4 exbidv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) )
6 dfac4 ⊢ ( CHOICE ↔ ∀ 𝑦 ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) )
7 6 axaci ⊢ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )
8 1 5 7 vtocl ⊢ ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )