Theorem dfac8a

Description: Numeration theorem: every set with a choice function on its power set is numerable. With AC, this reduces to the statement that every set is numerable. Similar to Theorem 10.3 of TakeutiZaring p. 84. (Contributed by NM, 10-Feb-1997) (Revised by Mario Carneiro, 5-Jan-2013)

	Ref	Expression
Assertion	dfac8a	$$⊢A\in B\to \left(\exists h\forall y\in 𝒫A\left(y\ne \varnothing \to h\left(y\right)\in y\right)\to A\in \mathrm{dom}\mathrm{card}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{recs}\left(\left(v\in \mathrm{V}⟼h\left(A\setminus \mathrm{ran}v\right)\right)\right)=\mathrm{recs}\left(\left(v\in \mathrm{V}⟼h\left(A\setminus \mathrm{ran}v\right)\right)\right)$$
2		rneq	$$⊢v=f\to \mathrm{ran}v=\mathrm{ran}f$$
3	2	difeq2d	$$⊢v=f\to A\setminus \mathrm{ran}v=A\setminus \mathrm{ran}f$$
4	3	fveq2d	$$⊢v=f\to h\left(A\setminus \mathrm{ran}v\right)=h\left(A\setminus \mathrm{ran}f\right)$$
5	4	cbvmptv	$$⊢\left(v\in \mathrm{V}⟼h\left(A\setminus \mathrm{ran}v\right)\right)=\left(f\in \mathrm{V}⟼h\left(A\setminus \mathrm{ran}f\right)\right)$$
6	1 5	dfac8alem	$$⊢A\in B\to \left(\exists h\forall y\in 𝒫A\left(y\ne \varnothing \to h\left(y\right)\in y\right)\to A\in \mathrm{dom}\mathrm{card}\right)$$