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\approx \mathrm{\omega }\to \exists f\forall z\in x\left(z\ne \varnothing \to f\left(z\right)\in z\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢x\setminus \left\{\varnothing \right\}=x\setminus \left\{\varnothing \right\}$$
2		eqid	$$⊢\left(t\in \mathrm{\omega },y\in \bigcup \left(x\setminus \left\{\varnothing \right\}\right)⟼v\left(t\right)\right)=\left(t\in \mathrm{\omega },y\in \bigcup \left(x\setminus \left\{\varnothing \right\}\right)⟼v\left(t\right)\right)$$
3		eqid	$$⊢\left(w\in \left(x\setminus \left\{\varnothing \right\}\right)⟼u\left(\mathrm{suc}{v}^{-1}\left(w\right)\right)\right)=\left(w\in \left(x\setminus \left\{\varnothing \right\}\right)⟼u\left(\mathrm{suc}{v}^{-1}\left(w\right)\right)\right)$$
4	1 2 3	axcclem	$$⊢x\approx \mathrm{\omega }\to \exists f\forall z\in x\left(z\ne \varnothing \to f\left(z\right)\in z\right)$$