Database
ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY
ZFC Set Theory - add the Axiom of Choice
Introduce the Axiom of Choice
axac3
Metamath Proof Explorer
Description: This theorem asserts that the constant CHOICE is a theorem, thus
eliminating it as a hypothesis while assuming ax-ac2 as an axiom.
(Contributed by Mario Carneiro , 6-May-2015) (Revised by NM , 20-Dec-2016) (Proof modification is discouraged.)
Ref
Expression
Assertion
axac3
⊢ CHOICE
Proof
Step
Hyp
Ref
Expression
1
ax-ac2
⊢ ∃ 𝑦 ∀ 𝑧 ∃ 𝑤 ∀ 𝑣 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑤 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑤 ) ∧ 𝑧 ∈ 𝑤 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑤 ∈ 𝑧 ∧ 𝑤 ∈ 𝑦 ) ∧ ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) → 𝑣 = 𝑤 ) ) ) ) )
2
1
ax-gen
⊢ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑤 ∀ 𝑣 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑤 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑤 ) ∧ 𝑧 ∈ 𝑤 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑤 ∈ 𝑧 ∧ 𝑤 ∈ 𝑦 ) ∧ ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) → 𝑣 = 𝑤 ) ) ) ) )
3
dfackm
⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑤 ∀ 𝑣 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑤 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑤 ) ∧ 𝑧 ∈ 𝑤 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑤 ∈ 𝑧 ∧ 𝑤 ∈ 𝑦 ) ∧ ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) → 𝑣 = 𝑤 ) ) ) ) ) )
4
2 3
mpbir
⊢ CHOICE