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	⊢ ( 𝐴 ≈ 𝐵 → AC 𝐴 = AC 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ensym	⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴 )
2		endom	⊢ ( 𝐵 ≈ 𝐴 → 𝐵 ≼ 𝐴 )
3		acndom	⊢ ( 𝐵 ≼ 𝐴 → ( 𝑥 ∈ AC 𝐴 → 𝑥 ∈ AC 𝐵 ) )
4	1 2 3	3syl	⊢ ( 𝐴 ≈ 𝐵 → ( 𝑥 ∈ AC 𝐴 → 𝑥 ∈ AC 𝐵 ) )
5		endom	⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵 )
6		acndom	⊢ ( 𝐴 ≼ 𝐵 → ( 𝑥 ∈ AC 𝐵 → 𝑥 ∈ AC 𝐴 ) )
7	5 6	syl	⊢ ( 𝐴 ≈ 𝐵 → ( 𝑥 ∈ AC 𝐵 → 𝑥 ∈ AC 𝐴 ) )
8	4 7	impbid	⊢ ( 𝐴 ≈ 𝐵 → ( 𝑥 ∈ AC 𝐴 ↔ 𝑥 ∈ AC 𝐵 ) )
9	8	eqrdv	⊢ ( 𝐴 ≈ 𝐵 → AC 𝐴 = AC 𝐵 )