Theorem acnen2

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

	Ref	Expression
Assertion	acnen2	$$⊢X\approx Y\to \left(X\in \underset{\_}{\mathrm{AC}}A\leftrightarrow Y\in \underset{\_}{\mathrm{AC}}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ensym	$$⊢X\approx Y\to Y\approx X$$
2		endom	$$⊢Y\approx X\to Y\preccurlyeq X$$
3		acndom2	$$⊢Y\preccurlyeq X\to \left(X\in \underset{\_}{\mathrm{AC}}A\to Y\in \underset{\_}{\mathrm{AC}}A\right)$$
4	1 2 3	3syl	$$⊢X\approx Y\to \left(X\in \underset{\_}{\mathrm{AC}}A\to Y\in \underset{\_}{\mathrm{AC}}A\right)$$
5		endom	$$⊢X\approx Y\to X\preccurlyeq Y$$
6		acndom2	$$⊢X\preccurlyeq Y\to \left(Y\in \underset{\_}{\mathrm{AC}}A\to X\in \underset{\_}{\mathrm{AC}}A\right)$$
7	5 6	syl	$$⊢X\approx Y\to \left(Y\in \underset{\_}{\mathrm{AC}}A\to X\in \underset{\_}{\mathrm{AC}}A\right)$$
8	4 7	impbid	$$⊢X\approx Y\to \left(X\in \underset{\_}{\mathrm{AC}}A\leftrightarrow Y\in \underset{\_}{\mathrm{AC}}A\right)$$