Metamath Proof Explorer

Theorem limsucncmp

Description: The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015)

Ref Expression
Assertion limsucncmp 
|- ( Lim A -> -. suc A e. Comp )

Proof

Step Hyp Ref Expression
1 suceq 
 |-  ( A = if ( Lim A , A , On ) -> suc A = suc if ( Lim A , A , On ) )
2 1 eleq1d 
 |-  ( A = if ( Lim A , A , On ) -> ( suc A e. Comp <-> suc if ( Lim A , A , On ) e. Comp ) )
3 2 notbid 
 |-  ( A = if ( Lim A , A , On ) -> ( -. suc A e. Comp <-> -. suc if ( Lim A , A , On ) e. Comp ) )
4 limeq 
 |-  ( A = if ( Lim A , A , On ) -> ( Lim A <-> Lim if ( Lim A , A , On ) ) )
5 limeq 
 |-  ( On = if ( Lim A , A , On ) -> ( Lim On <-> Lim if ( Lim A , A , On ) ) )
6 limon 
 |-  Lim On
7 4 5 6 elimhyp 
 |-  Lim if ( Lim A , A , On )
8 7 limsucncmpi 
 |-  -. suc if ( Lim A , A , On ) e. Comp
9 3 8 dedth 
 |-  ( Lim A -> -. suc A e. Comp )