Metamath Proof Explorer

Theorem alephdom2

Description: A dominated initial ordinal is included. (Contributed by Jeff Hankins, 24-Oct-2009)

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

Proof

Step Hyp Ref Expression
1 alephsdom 
 |-  ( ( B e. On /\ A e. On ) -> ( B e. ( aleph ` A ) <-> B ~< ( aleph ` A ) ) )
2 1 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> ( B e. ( aleph ` A ) <-> B ~< ( aleph ` A ) ) )
3 2 notbid 
 |-  ( ( A e. On /\ B e. On ) -> ( -. B e. ( aleph ` A ) <-> -. B ~< ( aleph ` A ) ) )
4 alephon 
 |-  ( aleph ` A ) e. On
5 4 onordi 
 |-  Ord ( aleph ` A )
6 eloni 
 |-  ( B e. On -> Ord B )
7 ordtri1 
 |-  ( ( Ord ( aleph ` A ) /\ Ord B ) -> ( ( aleph ` A ) C_ B <-> -. B e. ( aleph ` A ) ) )
8 5 6 7 sylancr 
 |-  ( B e. On -> ( ( aleph ` A ) C_ B <-> -. B e. ( aleph ` A ) ) )
9 8 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) C_ B <-> -. B e. ( aleph ` A ) ) )
10 domtriord 
 |-  ( ( ( aleph ` A ) e. On /\ B e. On ) -> ( ( aleph ` A ) ~<_ B <-> -. B ~< ( aleph ` A ) ) )
11 4 10 mpan 
 |-  ( B e. On -> ( ( aleph ` A ) ~<_ B <-> -. B ~< ( aleph ` A ) ) )
12 11 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) ~<_ B <-> -. B ~< ( aleph ` A ) ) )
13 3 9 12 3bitr4d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) C_ B <-> ( aleph ` A ) ~<_ B ) )