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 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 Comp suc if Lim A A On Comp
3 2 notbid A = if Lim A A On ¬ suc A Comp ¬ suc if Lim A A On 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 Comp
9 3 8 dedth Lim A ¬ suc A Comp