Metamath Proof Explorer

Theorem dfackm

Description: Equivalence of the Axiom of Choice and Maes' AC ackm . The proof consists of lemmas kmlem1 through kmlem16 and this final theorem. AC is not used for the proof. Note: bypassing the first step (i.e., replacing dfac5 with biid ) establishes the AC equivalence shown by Maes' writeup. The left-hand-side AC shown here was chosen because it is shorter to display. (Contributed by NM, 13-Apr-2004) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion dfackm ⊢ CHOICE ↔ ∀ x ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ∨ ¬ y ∈ x ∧ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v

Proof

Step Hyp Ref Expression
1 dfac5 ⊢ CHOICE ↔ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y
2 eqid ⊢ t | ∃ h ∈ x t = h ∖ ⋃ x ∖ h = t | ∃ h ∈ x t = h ∖ ⋃ x ∖ h
3 2 kmlem13 ⊢ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ x ¬ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w → ∃ y ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ y
4 kmlem8 ⊢ ¬ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w → ∃ y ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ y ↔ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ∨ ∃ y ¬ y ∈ x ∧ ∀ z ∈ x ∃! v v ∈ z ∩ y
5 4 albii ⊢ ∀ x ¬ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w → ∃ y ∀ z ∈ x z ≠ ∅ → ∃! v v ∈ z ∩ y ↔ ∀ x ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ∨ ∃ y ¬ y ∈ x ∧ ∀ z ∈ x ∃! v v ∈ z ∩ y
6 3 5 bitri ⊢ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ x ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ∨ ∃ y ¬ y ∈ x ∧ ∀ z ∈ x ∃! v v ∈ z ∩ y
7 df-ne ⊢ y ≠ v ↔ ¬ y = v
8 7 bicomi ⊢ ¬ y = v ↔ y ≠ v
9 8 anbi2i ⊢ v ∈ x ∧ ¬ y = v ↔ v ∈ x ∧ y ≠ v
10 9 anbi1i ⊢ v ∈ x ∧ ¬ y = v ∧ z ∈ v ↔ v ∈ x ∧ y ≠ v ∧ z ∈ v
11 10 imbi2i ⊢ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ↔ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ v
12 biid ⊢ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v ↔ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
13 biid ⊢ ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ z ∈ x ∃! v v ∈ z ∩ y
14 11 12 13 kmlem16 ⊢ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ∨ ∃ y ¬ y ∈ x ∧ ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ∨ ¬ y ∈ x ∧ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
15 14 albii ⊢ ∀ x ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ∨ ∃ y ¬ y ∈ x ∧ ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ x ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ∨ ¬ y ∈ x ∧ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
16 6 15 bitri ⊢ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y ↔ ∀ x ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ∨ ¬ y ∈ x ∧ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
17 1 16 bitri ⊢ CHOICE ↔ ∀ x ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ∨ ¬ y ∈ x ∧ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v