Metamath Proof Explorer

Theorem winafp

Description: A nontrivial weakly inaccessible cardinal is a fixed point of the aleph function. (Contributed by Mario Carneiro, 29-May-2014)

Ref Expression
Assertion winafp 
|- ( ( A e. InaccW /\ A =/= _om ) -> ( aleph ` A ) = A )

Proof

Step Hyp Ref Expression
1 winalim2 
 |-  ( ( A e. InaccW /\ A =/= _om ) -> E. x ( ( aleph ` x ) = A /\ Lim x ) )
2 vex 
 |-  x e. _V
3 limelon 
 |-  ( ( x e. _V /\ Lim x ) -> x e. On )
4 2 3 mpan 
 |-  ( Lim x -> x e. On )
5 alephle 
 |-  ( x e. On -> x C_ ( aleph ` x ) )
6 4 5 syl 
 |-  ( Lim x -> x C_ ( aleph ` x ) )
7 6 ad2antll 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( ( aleph ` x ) = A /\ Lim x ) ) -> x C_ ( aleph ` x ) )
8 simprl 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( ( aleph ` x ) = A /\ Lim x ) ) -> ( aleph ` x ) = A )
9 7 8 sseqtrd 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( ( aleph ` x ) = A /\ Lim x ) ) -> x C_ A )
10 8 fveq2d 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( ( aleph ` x ) = A /\ Lim x ) ) -> ( cf ` ( aleph ` x ) ) = ( cf ` A ) )
11 alephsing 
 |-  ( Lim x -> ( cf ` ( aleph ` x ) ) = ( cf ` x ) )
12 11 ad2antll 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( ( aleph ` x ) = A /\ Lim x ) ) -> ( cf ` ( aleph ` x ) ) = ( cf ` x ) )
13 10 12 eqtr3d 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( ( aleph ` x ) = A /\ Lim x ) ) -> ( cf ` A ) = ( cf ` x ) )
14 elwina 
 |-  ( A e. InaccW <-> ( A =/= (/) /\ ( cf ` A ) = A /\ A. y e. A E. z e. A y ~< z ) )
15 14 simp2bi 
 |-  ( A e. InaccW -> ( cf ` A ) = A )
16 15 ad2antrr 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( ( aleph ` x ) = A /\ Lim x ) ) -> ( cf ` A ) = A )
17 13 16 eqtr3d 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( ( aleph ` x ) = A /\ Lim x ) ) -> ( cf ` x ) = A )
18 cfle 
 |-  ( cf ` x ) C_ x
19 17 18 eqsstrrdi 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( ( aleph ` x ) = A /\ Lim x ) ) -> A C_ x )
20 9 19 eqssd 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( ( aleph ` x ) = A /\ Lim x ) ) -> x = A )
21 20 fveq2d 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( ( aleph ` x ) = A /\ Lim x ) ) -> ( aleph ` x ) = ( aleph ` A ) )
22 21 8 eqtr3d 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( ( aleph ` x ) = A /\ Lim x ) ) -> ( aleph ` A ) = A )
23 1 22 exlimddv 
 |-  ( ( A e. InaccW /\ A =/= _om ) -> ( aleph ` A ) = A )