Metamath Proof Explorer


Theorem gchaleph

Description: If ( alephA ) is a GCH-set and its powerset is well-orderable, then the successor aleph ( alephsuc A ) is equinumerous to the powerset of ( alephA ) . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion gchaleph
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( aleph ` suc A ) ~~ ~P ( aleph ` A ) )

Proof

Step Hyp Ref Expression
1 alephsucpw2
 |-  -. ~P ( aleph ` A ) ~< ( aleph ` suc A )
2 alephon
 |-  ( aleph ` suc A ) e. On
3 onenon
 |-  ( ( aleph ` suc A ) e. On -> ( aleph ` suc A ) e. dom card )
4 2 3 ax-mp
 |-  ( aleph ` suc A ) e. dom card
5 simp3
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ~P ( aleph ` A ) e. dom card )
6 domtri2
 |-  ( ( ( aleph ` suc A ) e. dom card /\ ~P ( aleph ` A ) e. dom card ) -> ( ( aleph ` suc A ) ~<_ ~P ( aleph ` A ) <-> -. ~P ( aleph ` A ) ~< ( aleph ` suc A ) ) )
7 4 5 6 sylancr
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( ( aleph ` suc A ) ~<_ ~P ( aleph ` A ) <-> -. ~P ( aleph ` A ) ~< ( aleph ` suc A ) ) )
8 1 7 mpbiri
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( aleph ` suc A ) ~<_ ~P ( aleph ` A ) )
9 fvex
 |-  ( aleph ` A ) e. _V
10 simp1
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> A e. On )
11 alephgeom
 |-  ( A e. On <-> _om C_ ( aleph ` A ) )
12 10 11 sylib
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> _om C_ ( aleph ` A ) )
13 ssdomg
 |-  ( ( aleph ` A ) e. _V -> ( _om C_ ( aleph ` A ) -> _om ~<_ ( aleph ` A ) ) )
14 9 12 13 mpsyl
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> _om ~<_ ( aleph ` A ) )
15 domnsym
 |-  ( _om ~<_ ( aleph ` A ) -> -. ( aleph ` A ) ~< _om )
16 14 15 syl
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> -. ( aleph ` A ) ~< _om )
17 isfinite
 |-  ( ( aleph ` A ) e. Fin <-> ( aleph ` A ) ~< _om )
18 16 17 sylnibr
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> -. ( aleph ` A ) e. Fin )
19 simp2
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( aleph ` A ) e. GCH )
20 alephordilem1
 |-  ( A e. On -> ( aleph ` A ) ~< ( aleph ` suc A ) )
21 20 3ad2ant1
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( aleph ` A ) ~< ( aleph ` suc A ) )
22 gchi
 |-  ( ( ( aleph ` A ) e. GCH /\ ( aleph ` A ) ~< ( aleph ` suc A ) /\ ( aleph ` suc A ) ~< ~P ( aleph ` A ) ) -> ( aleph ` A ) e. Fin )
23 22 3expia
 |-  ( ( ( aleph ` A ) e. GCH /\ ( aleph ` A ) ~< ( aleph ` suc A ) ) -> ( ( aleph ` suc A ) ~< ~P ( aleph ` A ) -> ( aleph ` A ) e. Fin ) )
24 19 21 23 syl2anc
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( ( aleph ` suc A ) ~< ~P ( aleph ` A ) -> ( aleph ` A ) e. Fin ) )
25 18 24 mtod
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> -. ( aleph ` suc A ) ~< ~P ( aleph ` A ) )
26 domtri2
 |-  ( ( ~P ( aleph ` A ) e. dom card /\ ( aleph ` suc A ) e. dom card ) -> ( ~P ( aleph ` A ) ~<_ ( aleph ` suc A ) <-> -. ( aleph ` suc A ) ~< ~P ( aleph ` A ) ) )
27 5 4 26 sylancl
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( ~P ( aleph ` A ) ~<_ ( aleph ` suc A ) <-> -. ( aleph ` suc A ) ~< ~P ( aleph ` A ) ) )
28 25 27 mpbird
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ~P ( aleph ` A ) ~<_ ( aleph ` suc A ) )
29 sbth
 |-  ( ( ( aleph ` suc A ) ~<_ ~P ( aleph ` A ) /\ ~P ( aleph ` A ) ~<_ ( aleph ` suc A ) ) -> ( aleph ` suc A ) ~~ ~P ( aleph ` A ) )
30 8 28 29 syl2anc
 |-  ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( aleph ` suc A ) ~~ ~P ( aleph ` A ) )