Metamath Proof Explorer

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 ~~ Y -> ( X e. AC_ A <-> Y e. AC_ A ) )

Proof

Step Hyp Ref Expression
1 ensym 
 |-  ( X ~~ Y -> Y ~~ X )
2 endom 
 |-  ( Y ~~ X -> Y ~<_ X )
3 acndom2 
 |-  ( Y ~<_ X -> ( X e. AC_ A -> Y e. AC_ A ) )
4 1 2 3 3syl 
 |-  ( X ~~ Y -> ( X e. AC_ A -> Y e. AC_ A ) )
5 endom 
 |-  ( X ~~ Y -> X ~<_ Y )
6 acndom2 
 |-  ( X ~<_ Y -> ( Y e. AC_ A -> X e. AC_ A ) )
7 5 6 syl 
 |-  ( X ~~ Y -> ( Y e. AC_ A -> X e. AC_ A ) )
8 4 7 impbid 
 |-  ( X ~~ Y -> ( X e. AC_ A <-> Y e. AC_ A ) )