Metamath Proof Explorer

Theorem aleph11

Description: The aleph function is one-to-one. (Contributed by NM, 3-Aug-2004)

Ref Expression
Assertion aleph11 
|- ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) = ( aleph ` B ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 alephord3 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( aleph ` A ) C_ ( aleph ` B ) ) )
2 alephord3 
 |-  ( ( B e. On /\ A e. On ) -> ( B C_ A <-> ( aleph ` B ) C_ ( aleph ` A ) ) )
3 2 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> ( B C_ A <-> ( aleph ` B ) C_ ( aleph ` A ) ) )
4 1 3 anbi12d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A C_ B /\ B C_ A ) <-> ( ( aleph ` A ) C_ ( aleph ` B ) /\ ( aleph ` B ) C_ ( aleph ` A ) ) ) )
5 eqss 
 |-  ( A = B <-> ( A C_ B /\ B C_ A ) )
6 eqss 
 |-  ( ( aleph ` A ) = ( aleph ` B ) <-> ( ( aleph ` A ) C_ ( aleph ` B ) /\ ( aleph ` B ) C_ ( aleph ` A ) ) )
7 4 5 6 3bitr4g 
 |-  ( ( A e. On /\ B e. On ) -> ( A = B <-> ( aleph ` A ) = ( aleph ` B ) ) )
8 7 bicomd 
 |-  ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) = ( aleph ` B ) <-> A = B ) )