Metamath Proof Explorer

Theorem alephsucdom

Description: A set dominated by an aleph is strictly dominated by its successor aleph and vice-versa. (Contributed by NM, 3-Nov-2003) (Revised by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion alephsucdom 
|- ( B e. On -> ( A ~<_ ( aleph ` B ) <-> A ~< ( aleph ` suc B ) ) )

Proof

Step Hyp Ref Expression
1 alephordilem1 
 |-  ( B e. On -> ( aleph ` B ) ~< ( aleph ` suc B ) )
2 domsdomtr 
 |-  ( ( A ~<_ ( aleph ` B ) /\ ( aleph ` B ) ~< ( aleph ` suc B ) ) -> A ~< ( aleph ` suc B ) )
3 2 ex 
 |-  ( A ~<_ ( aleph ` B ) -> ( ( aleph ` B ) ~< ( aleph ` suc B ) -> A ~< ( aleph ` suc B ) ) )
4 1 3 syl5com 
 |-  ( B e. On -> ( A ~<_ ( aleph ` B ) -> A ~< ( aleph ` suc B ) ) )
5 sdomdom 
 |-  ( A ~< ( aleph ` suc B ) -> A ~<_ ( aleph ` suc B ) )
6 alephon 
 |-  ( aleph ` suc B ) e. On
7 ondomen 
 |-  ( ( ( aleph ` suc B ) e. On /\ A ~<_ ( aleph ` suc B ) ) -> A e. dom card )
8 6 7 mpan 
 |-  ( A ~<_ ( aleph ` suc B ) -> A e. dom card )
9 cardid2 
 |-  ( A e. dom card -> ( card ` A ) ~~ A )
10 5 8 9 3syl 
 |-  ( A ~< ( aleph ` suc B ) -> ( card ` A ) ~~ A )
11 10 ensymd 
 |-  ( A ~< ( aleph ` suc B ) -> A ~~ ( card ` A ) )
12 alephnbtwn2 
 |-  -. ( ( aleph ` B ) ~< ( card ` A ) /\ ( card ` A ) ~< ( aleph ` suc B ) )
13 12 imnani 
 |-  ( ( aleph ` B ) ~< ( card ` A ) -> -. ( card ` A ) ~< ( aleph ` suc B ) )
14 ensdomtr 
 |-  ( ( ( card ` A ) ~~ A /\ A ~< ( aleph ` suc B ) ) -> ( card ` A ) ~< ( aleph ` suc B ) )
15 10 14 mpancom 
 |-  ( A ~< ( aleph ` suc B ) -> ( card ` A ) ~< ( aleph ` suc B ) )
16 13 15 nsyl3 
 |-  ( A ~< ( aleph ` suc B ) -> -. ( aleph ` B ) ~< ( card ` A ) )
17 cardon 
 |-  ( card ` A ) e. On
18 alephon 
 |-  ( aleph ` B ) e. On
19 domtriord 
 |-  ( ( ( card ` A ) e. On /\ ( aleph ` B ) e. On ) -> ( ( card ` A ) ~<_ ( aleph ` B ) <-> -. ( aleph ` B ) ~< ( card ` A ) ) )
20 17 18 19 mp2an 
 |-  ( ( card ` A ) ~<_ ( aleph ` B ) <-> -. ( aleph ` B ) ~< ( card ` A ) )
21 16 20 sylibr 
 |-  ( A ~< ( aleph ` suc B ) -> ( card ` A ) ~<_ ( aleph ` B ) )
22 endomtr 
 |-  ( ( A ~~ ( card ` A ) /\ ( card ` A ) ~<_ ( aleph ` B ) ) -> A ~<_ ( aleph ` B ) )
23 11 21 22 syl2anc 
 |-  ( A ~< ( aleph ` suc B ) -> A ~<_ ( aleph ` B ) )
24 4 23 impbid1 
 |-  ( B e. On -> ( A ~<_ ( aleph ` B ) <-> A ~< ( aleph ` suc B ) ) )