Theorem acnen

Description: The class of choice sets of length A is a cardinal invariant. (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	acnen	$$⊢A\approx B\to \underset{\_}{\mathrm{AC}}A=\underset{\_}{\mathrm{AC}}B$$

Proof

Step	Hyp	Ref	Expression
1		ensym	$$⊢A\approx B\to B\approx A$$
2		endom	$$⊢B\approx A\to B\preccurlyeq A$$
3		acndom	$$⊢B\preccurlyeq A\to \left(x\in \underset{\_}{\mathrm{AC}}A\to x\in \underset{\_}{\mathrm{AC}}B\right)$$
4	1 2 3	3syl	$$⊢A\approx B\to \left(x\in \underset{\_}{\mathrm{AC}}A\to x\in \underset{\_}{\mathrm{AC}}B\right)$$
5		endom	$$⊢A\approx B\to A\preccurlyeq B$$
6		acndom	$$⊢A\preccurlyeq B\to \left(x\in \underset{\_}{\mathrm{AC}}B\to x\in \underset{\_}{\mathrm{AC}}A\right)$$
7	5 6	syl	$$⊢A\approx B\to \left(x\in \underset{\_}{\mathrm{AC}}B\to x\in \underset{\_}{\mathrm{AC}}A\right)$$
8	4 7	impbid	$$⊢A\approx B\to \left(x\in \underset{\_}{\mathrm{AC}}A\leftrightarrow x\in \underset{\_}{\mathrm{AC}}B\right)$$
9	8	eqrdv	$$⊢A\approx B\to \underset{\_}{\mathrm{AC}}A=\underset{\_}{\mathrm{AC}}B$$