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

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 ↔ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfac5 ⊢ ( CHOICE ↔ ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
2 eqid ⊢ { 𝑡 ∣ ∃ ℎ ∈ 𝑥 𝑡 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) } = { 𝑡 ∣ ∃ ℎ ∈ 𝑥 𝑡 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) }
3 2 kmlem13 ⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
4 kmlem8 ⊢ ( ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
5 4 albii ⊢ ( ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ 𝑥 ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
6 3 5 bitri ⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
7 df-ne ⊢ ( 𝑦 ≠ 𝑣 ↔ ¬ 𝑦 = 𝑣 )
8 7 bicomi ⊢ ( ¬ 𝑦 = 𝑣 ↔ 𝑦 ≠ 𝑣 )
9 8 anbi2i ⊢ ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ↔ ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) )
10 9 anbi1i ⊢ ( ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ↔ ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) )
11 10 imbi2i ⊢ ( ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ↔ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) )
12 biid ⊢ ( ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ↔ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
13 biid ⊢ ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )
14 11 12 13 kmlem16 ⊢ ( ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) ) )
15 14 albii ⊢ ( ∀ 𝑥 ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) ) )
16 6 15 bitri ⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) ) )
17 1 16 bitri ⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) ) )