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		simpr	$$⊢\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 \left(𝒫X\setminus \left\{\varnothing \right\}\right)f\left(x\right)\in x$$
15	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)$$
16		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)$$
17	15 16	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)$$
18	17	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)$$
19	14 18	sylib	$$⊢\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)$$
20	19	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)$$
21	13 20	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)$$
22		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)$$
23	21 22	mpd	$$⊢X\in \underset{\_}{\mathrm{AC}}𝒫X\to X\in \mathrm{dom}\mathrm{card}$$
24		pwexg	$$⊢X\in \mathrm{dom}\mathrm{card}\to 𝒫X\in \mathrm{V}$$
25		numacn	$$⊢𝒫X\in \mathrm{V}\to \left(X\in \mathrm{dom}\mathrm{card}\to X\in \underset{\_}{\mathrm{AC}}𝒫X\right)$$
26	24 25	mpcom	$$⊢X\in \mathrm{dom}\mathrm{card}\to X\in \underset{\_}{\mathrm{AC}}𝒫X$$
27	23 26	impbii	$$⊢X\in \underset{\_}{\mathrm{AC}}𝒫X\leftrightarrow X\in \mathrm{dom}\mathrm{card}$$