Theorem acacni

Description: A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	acacni	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to \underset{\_}{\mathrm{AC}}A=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to A\in V$$
2		vex	$$⊢x\in \mathrm{V}$$
3		simpl	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to \mathrm{CHOICE}$$
4		dfac10	$$⊢\mathrm{CHOICE}\leftrightarrow \mathrm{dom}\mathrm{card}=\mathrm{V}$$
5	3 4	sylib	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to \mathrm{dom}\mathrm{card}=\mathrm{V}$$
6	2 5	eleqtrrid	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to x\in \mathrm{dom}\mathrm{card}$$
7		numacn	$$⊢A\in V\to \left(x\in \mathrm{dom}\mathrm{card}\to x\in \underset{\_}{\mathrm{AC}}A\right)$$
8	1 6 7	sylc	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to x\in \underset{\_}{\mathrm{AC}}A$$
9	2	a1i	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to x\in \mathrm{V}$$
10	8 9	2thd	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to \left(x\in \underset{\_}{\mathrm{AC}}A\leftrightarrow x\in \mathrm{V}\right)$$
11	10	eqrdv	$$⊢\left(\mathrm{CHOICE}\wedge A\in V\right)\to \underset{\_}{\mathrm{AC}}A=\mathrm{V}$$