Theorem axdc2

Description: An apparent strengthening of ax-dc (but derived from it) which shows that there is a denumerable sequence g for any function that maps elements of a set A to nonempty subsets of A such that g ( x + 1 ) e. F ( g ( x ) ) for all x e. _om . The finitistic version of this can be proven by induction, but the infinite version requires this new axiom. (Contributed by Mario Carneiro, 25-Jan-2013)

	Ref	Expression
Hypothesis	axdc2.1	$$⊢A\in \mathrm{V}$$
Assertion	axdc2	$$⊢\left(A\ne \varnothing \wedge F:A⟶𝒫A\setminus \left\{\varnothing \right\}\right)\to \exists g\left(g:\mathrm{\omega }⟶A\wedge \forall k\in \mathrm{\omega }g\left(\mathrm{suc}k\right)\in F\left(g\left(k\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		axdc2.1	$$⊢A\in \mathrm{V}$$
2		eleq1w	$$⊢s=x\to \left(s\in A\leftrightarrow x\in A\right)$$
3	2	adantr	$$⊢\left(s=x\wedge t=y\right)\to \left(s\in A\leftrightarrow x\in A\right)$$
4		fveq2	$$⊢s=x\to F\left(s\right)=F\left(x\right)$$
5	4	eleq2d	$$⊢s=x\to \left(t\in F\left(s\right)\leftrightarrow t\in F\left(x\right)\right)$$
6		eleq1w	$$⊢t=y\to \left(t\in F\left(x\right)\leftrightarrow y\in F\left(x\right)\right)$$
7	5 6	sylan9bb	$$⊢\left(s=x\wedge t=y\right)\to \left(t\in F\left(s\right)\leftrightarrow y\in F\left(x\right)\right)$$
8	3 7	anbi12d	$$⊢\left(s=x\wedge t=y\right)\to \left(\left(s\in A\wedge t\in F\left(s\right)\right)\leftrightarrow \left(x\in A\wedge y\in F\left(x\right)\right)\right)$$
9	8	cbvopabv	$$⊢\left\{⟨s,t⟩|\left(s\in A\wedge t\in F\left(s\right)\right)\right\}=\left\{⟨x,y⟩|\left(x\in A\wedge y\in F\left(x\right)\right)\right\}$$
10		fveq2	$$⊢n=x\to h\left(n\right)=h\left(x\right)$$
11	10	cbvmptv	$$⊢\left(n\in \mathrm{\omega }⟼h\left(n\right)\right)=\left(x\in \mathrm{\omega }⟼h\left(x\right)\right)$$
12	1 9 11	axdc2lem	$$⊢\left(A\ne \varnothing \wedge F:A⟶𝒫A\setminus \left\{\varnothing \right\}\right)\to \exists g\left(g:\mathrm{\omega }⟶A\wedge \forall k\in \mathrm{\omega }g\left(\mathrm{suc}k\right)\in F\left(g\left(k\right)\right)\right)$$