This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )