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

Metamath Proof Explorer

Theorem axac2

Description: Derive ax-ac2 from ax-ac . (Contributed by NM, 19-Dec-2016) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion axac2 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfac2a ⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) → CHOICE )
2 ac3 ⊢ ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) )
3 1 2 mpg ⊢ CHOICE
4 dfackm ⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) ) )
5 3 4 mpbi ⊢ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )
6 5 spi ⊢ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )