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	⊢ ( 𝑥 ≈ ω → ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑥 ∖ { ∅ } ) = ( 𝑥 ∖ { ∅ } )
2		eqid	⊢ ( 𝑡 ∈ ω , 𝑦 ∈ ∪ ( 𝑥 ∖ { ∅ } ) ↦ ( 𝑣 ‘ 𝑡 ) ) = ( 𝑡 ∈ ω , 𝑦 ∈ ∪ ( 𝑥 ∖ { ∅ } ) ↦ ( 𝑣 ‘ 𝑡 ) )
3		eqid	⊢ ( 𝑤 ∈ ( 𝑥 ∖ { ∅ } ) ↦ ( 𝑢 ‘ suc ( ◡ 𝑣 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( 𝑥 ∖ { ∅ } ) ↦ ( 𝑢 ‘ suc ( ◡ 𝑣 ‘ 𝑤 ) ) )
4	1 2 3	axcclem	⊢ ( 𝑥 ≈ ω → ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )