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 𝐴 → ¬ suc 𝐴 ∈ Comp )

Proof

Step	Hyp	Ref	Expression
1		suceq	⊢ ( 𝐴 = if ( Lim 𝐴 , 𝐴 , On ) → suc 𝐴 = suc if ( Lim 𝐴 , 𝐴 , On ) )
2	1	eleq1d	⊢ ( 𝐴 = if ( Lim 𝐴 , 𝐴 , On ) → ( suc 𝐴 ∈ Comp ↔ suc if ( Lim 𝐴 , 𝐴 , On ) ∈ Comp ) )
3	2	notbid	⊢ ( 𝐴 = if ( Lim 𝐴 , 𝐴 , On ) → ( ¬ suc 𝐴 ∈ Comp ↔ ¬ suc if ( Lim 𝐴 , 𝐴 , On ) ∈ Comp ) )
4		limeq	⊢ ( 𝐴 = if ( Lim 𝐴 , 𝐴 , On ) → ( Lim 𝐴 ↔ Lim if ( Lim 𝐴 , 𝐴 , On ) ) )
5		limeq	⊢ ( On = if ( Lim 𝐴 , 𝐴 , On ) → ( Lim On ↔ Lim if ( Lim 𝐴 , 𝐴 , On ) ) )
6		limon	⊢ Lim On
7	4 5 6	elimhyp	⊢ Lim if ( Lim 𝐴 , 𝐴 , On )
8	7	limsucncmpi	⊢ ¬ suc if ( Lim 𝐴 , 𝐴 , On ) ∈ Comp
9	3 8	dedth	⊢ ( Lim 𝐴 → ¬ suc 𝐴 ∈ Comp )