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

Metamath Proof Explorer

Theorem axcc

Description: Although CC can be proven trivially using ac5 , we prove it here using DC. (New usage is discouraged.) (Contributed by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion axcc ⊢ x ≈ ω → ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ z

Proof

Step Hyp Ref Expression
1 eqid ⊢ x ∖ ∅ = x ∖ ∅
2 eqid ⊢ t ∈ ω , y ∈ ⋃ x ∖ ∅ ⟼ v ⁡ t = t ∈ ω , y ∈ ⋃ x ∖ ∅ ⟼ v ⁡ t
3 eqid ⊢ w ∈ x ∖ ∅ ⟼ u ⁡ suc ⁡ v -1 ⁡ w = w ∈ x ∖ ∅ ⟼ u ⁡ suc ⁡ v -1 ⁡ w
4 1 2 3 axcclem ⊢ x ≈ ω → ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ z