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∀uy∈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∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y
2 eqid ⊢t|∃h∈xt=h∖⋃x∖h=t|∃h∈xt=h∖⋃x∖h
3 2 kmlem13 ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y↔∀x¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y
4 kmlem8 ⊢¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y↔∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w∨∃y¬y∈x∧∀z∈x∃!vv∈z∩y
5 4 albii ⊢∀x¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w→∃y∀z∈xz≠∅→∃!vv∈z∩y↔∀x∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w∨∃y¬y∈x∧∀z∈x∃!vv∈z∩y
6 3 5 bitri ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y↔∀x∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w∨∃y¬y∈x∧∀z∈x∃!vv∈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∃!vv∈z∩y↔∀z∈x∃!vv∈z∩y
14 11 12 13 kmlem16 ⊢∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w∨∃y¬y∈x∧∀z∈x∃!vv∈z∩y↔∃y∀z∃v∀uy∈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∈xz≠w∧v∈z∩w∨∃y¬y∈x∧∀z∈x∃!vv∈z∩y↔∀x∃y∀z∃v∀uy∈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∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∃y∀z∈x∃!vv∈z∩y↔∀x∃y∀z∃v∀uy∈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∀uy∈x∧z∈y→v∈x∧¬y=v∧z∈v∨¬y∈x∧z∈x→v∈z∧v∈y∧u∈z∧u∈y→u=v