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 ~~ B -> AC_ A = AC_ B )

Proof

Step	Hyp	Ref	Expression
1		ensym	|- ( A ~~ B -> B ~~ A )
2		endom	|- ( B ~~ A -> B ~<_ A )
3		acndom	|- ( B ~<_ A -> ( x e. AC_ A -> x e. AC_ B ) )
4	1 2 3	3syl	|- ( A ~~ B -> ( x e. AC_ A -> x e. AC_ B ) )
5		endom	|- ( A ~~ B -> A ~<_ B )
6		acndom	|- ( A ~<_ B -> ( x e. AC_ B -> x e. AC_ A ) )
7	5 6	syl	|- ( A ~~ B -> ( x e. AC_ B -> x e. AC_ A ) )
8	4 7	impbid	|- ( A ~~ B -> ( x e. AC_ A <-> x e. AC_ B ) )
9	8	eqrdv	|- ( A ~~ B -> AC_ A = AC_ B )