Theorem acnnum

Description: A set X which has choice sequences on it of length ~P X is well-orderable (and hence has choice sequences of every length). (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	acnnum	$$⊢X\in \underset{\_}{\mathrm{AC}}𝒫X\leftrightarrow X\in \mathrm{dom}\mathrm{card}$$

Proof

Step	Hyp	Ref	Expression
1		pwexg	$$⊢X\in \underset{\_}{\mathrm{AC}}𝒫X\to 𝒫X\in \mathrm{V}$$
2		difss	$$⊢𝒫X\setminus \left\{\varnothing \right\}\subseteq 𝒫X$$
3		ssdomg	$$⊢𝒫X\in \mathrm{V}\to \left(𝒫X\setminus \left\{\varnothing \right\}\subseteq 𝒫X\to \left(𝒫X\setminus \left\{\varnothing \right\}\right)\preccurlyeq 𝒫X\right)$$
4	1 2 3	mpisyl	$$⊢X\in \underset{\_}{\mathrm{AC}}𝒫X\to \left(𝒫X\setminus \left\{\varnothing \right\}\right)\preccurlyeq 𝒫X$$
5		acndom	$$⊢\left(𝒫X\setminus \left\{\varnothing \right\}\right)\preccurlyeq 𝒫X\to \left(X\in \underset{\_}{\mathrm{AC}}𝒫X\to X\in \underset{\_}{\mathrm{AC}}\left(𝒫X\setminus \left\{\varnothing \right\}\right)\right)$$
6	4 5	mpcom	$$⊢X\in \underset{\_}{\mathrm{AC}}𝒫X\to X\in \underset{\_}{\mathrm{AC}}\left(𝒫X\setminus \left\{\varnothing \right\}\right)$$
7		eldifsn	$$⊢x\in \left(𝒫X\setminus \left\{\varnothing \right\}\right)\leftrightarrow \left(x\in 𝒫X\wedge x\ne \varnothing \right)$$
8		elpwi	$$⊢x\in 𝒫X\to x\subseteq X$$
9	8	anim1i	$$⊢\left(x\in 𝒫X\wedge x\ne \varnothing \right)\to \left(x\subseteq X\wedge x\ne \varnothing \right)$$
10	7 9	sylbi	$$⊢x\in \left(𝒫X\setminus \left\{\varnothing \right\}\right)\to \left(x\subseteq X\wedge x\ne \varnothing \right)$$
11	10	rgen	$$⊢\forall x\in \left(𝒫X\setminus \left\{\varnothing \right\}\right)\left(x\subseteq X\wedge x\ne \varnothing \right)$$
12		acni2	$$⊢\left(X\in \underset{\_}{\mathrm{AC}}\left(𝒫X\setminus \left\{\varnothing \right\}\right)\wedge \forall x\in \left(𝒫X\setminus \left\{\varnothing \right\}\right)\left(x\subseteq X\wedge x\ne \varnothing \right)\right)\to \exists f\left(f:𝒫X\setminus \left\{\varnothing \right\}⟶X\wedge \forall x\in \left(𝒫X\setminus \left\{\varnothing \right\}\right)f\left(x\right)\in x\right)$$
13	6 11 12	sylancl	$$⊢X\in \underset{\_}{\mathrm{AC}}𝒫X\to \exists f\left(f:𝒫X\setminus \left\{\varnothing \right\}⟶X\wedge \forall x\in \left(𝒫X\setminus \left\{\varnothing \right\}\right)f\left(x\right)\in x\right)$$
14	7	imbi1i	$$⊢\left(x\in \left(𝒫X\setminus \left\{\varnothing \right\}\right)\to f\left(x\right)\in x\right)\leftrightarrow \left(\left(x\in 𝒫X\wedge x\ne \varnothing \right)\to f\left(x\right)\in x\right)$$
15		impexp	$$⊢\left(\left(x\in 𝒫X\wedge x\ne \varnothing \right)\to f\left(x\right)\in x\right)\leftrightarrow \left(x\in 𝒫X\to \left(x\ne \varnothing \to f\left(x\right)\in x\right)\right)$$
16	14 15	bitri	$$⊢\left(x\in \left(𝒫X\setminus \left\{\varnothing \right\}\right)\to f\left(x\right)\in x\right)\leftrightarrow \left(x\in 𝒫X\to \left(x\ne \varnothing \to f\left(x\right)\in x\right)\right)$$
17	16	ralbii2	$$⊢\forall x\in \left(𝒫X\setminus \left\{\varnothing \right\}\right)f\left(x\right)\in x\leftrightarrow \forall x\in 𝒫X\left(x\ne \varnothing \to f\left(x\right)\in x\right)$$
18	17	bilani	$$⊢\left(f:𝒫X\setminus \left\{\varnothing \right\}⟶X\wedge \forall x\in \left(𝒫X\setminus \left\{\varnothing \right\}\right)f\left(x\right)\in x\right)\to \forall x\in 𝒫X\left(x\ne \varnothing \to f\left(x\right)\in x\right)$$
19	18	eximi	$$⊢\exists f\left(f:𝒫X\setminus \left\{\varnothing \right\}⟶X\wedge \forall x\in \left(𝒫X\setminus \left\{\varnothing \right\}\right)f\left(x\right)\in x\right)\to \exists f\forall x\in 𝒫X\left(x\ne \varnothing \to f\left(x\right)\in x\right)$$
20	13 19	syl	$$⊢X\in \underset{\_}{\mathrm{AC}}𝒫X\to \exists f\forall x\in 𝒫X\left(x\ne \varnothing \to f\left(x\right)\in x\right)$$
21		dfac8a	$$⊢X\in \underset{\_}{\mathrm{AC}}𝒫X\to \left(\exists f\forall x\in 𝒫X\left(x\ne \varnothing \to f\left(x\right)\in x\right)\to X\in \mathrm{dom}\mathrm{card}\right)$$
22	20 21	mpd	$$⊢X\in \underset{\_}{\mathrm{AC}}𝒫X\to X\in \mathrm{dom}\mathrm{card}$$
23		pwexg	$$⊢X\in \mathrm{dom}\mathrm{card}\to 𝒫X\in \mathrm{V}$$
24		numacn	$$⊢𝒫X\in \mathrm{V}\to \left(X\in \mathrm{dom}\mathrm{card}\to X\in \underset{\_}{\mathrm{AC}}𝒫X\right)$$
25	23 24	mpcom	$$⊢X\in \mathrm{dom}\mathrm{card}\to X\in \underset{\_}{\mathrm{AC}}𝒫X$$
26	22 25	impbii	$$⊢X\in \underset{\_}{\mathrm{AC}}𝒫X\leftrightarrow X\in \mathrm{dom}\mathrm{card}$$