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	⊢ ( 𝑋 ≈ 𝑌 → ( 𝑋 ∈ AC 𝐴 ↔ 𝑌 ∈ AC 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ensym	⊢ ( 𝑋 ≈ 𝑌 → 𝑌 ≈ 𝑋 )
2		endom	⊢ ( 𝑌 ≈ 𝑋 → 𝑌 ≼ 𝑋 )
3		acndom2	⊢ ( 𝑌 ≼ 𝑋 → ( 𝑋 ∈ AC 𝐴 → 𝑌 ∈ AC 𝐴 ) )
4	1 2 3	3syl	⊢ ( 𝑋 ≈ 𝑌 → ( 𝑋 ∈ AC 𝐴 → 𝑌 ∈ AC 𝐴 ) )
5		endom	⊢ ( 𝑋 ≈ 𝑌 → 𝑋 ≼ 𝑌 )
6		acndom2	⊢ ( 𝑋 ≼ 𝑌 → ( 𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴 ) )
7	5 6	syl	⊢ ( 𝑋 ≈ 𝑌 → ( 𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴 ) )
8	4 7	impbid	⊢ ( 𝑋 ≈ 𝑌 → ( 𝑋 ∈ AC 𝐴 ↔ 𝑌 ∈ AC 𝐴 ) )