Metamath Proof Explorer

Theorem alephsdom

Description: If an ordinal is smaller than an initial ordinal, it is strictly dominated by it. (Contributed by Jeff Hankins, 24-Oct-2009) (Proof shortened by Mario Carneiro, 20-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. On /\ B e. On ) -> A e. On )
2 alephon 
 |-  ( aleph ` B ) e. On
3 onenon 
 |-  ( ( aleph ` B ) e. On -> ( aleph ` B ) e. dom card )
4 2 3 ax-mp 
 |-  ( aleph ` B ) e. dom card
5 cardsdomel 
 |-  ( ( A e. On /\ ( aleph ` B ) e. dom card ) -> ( A ~< ( aleph ` B ) <-> A e. ( card ` ( aleph ` B ) ) ) )
6 1 4 5 sylancl 
 |-  ( ( A e. On /\ B e. On ) -> ( A ~< ( aleph ` B ) <-> A e. ( card ` ( aleph ` B ) ) ) )
7 alephcard 
 |-  ( card ` ( aleph ` B ) ) = ( aleph ` B )
8 7 eleq2i 
 |-  ( A e. ( card ` ( aleph ` B ) ) <-> A e. ( aleph ` B ) )
9 6 8 bitr2di 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. ( aleph ` B ) <-> A ~< ( aleph ` B ) ) )