Theorem onsucsuccmp

Description: The successor of a successor ordinal number is a compact topology. (Contributed by Chen-Pang He, 18-Oct-2015)

	Ref	Expression
Assertion	onsucsuccmp	⊢ ( 𝐴 ∈ On → suc suc 𝐴 ∈ Comp )

Proof

Step	Hyp	Ref	Expression
1		suceq	⊢ ( 𝐴 = if ( 𝐴 ∈ On , 𝐴 , ∅ ) → suc 𝐴 = suc if ( 𝐴 ∈ On , 𝐴 , ∅ ) )
2		suceq	⊢ ( suc 𝐴 = suc if ( 𝐴 ∈ On , 𝐴 , ∅ ) → suc suc 𝐴 = suc suc if ( 𝐴 ∈ On , 𝐴 , ∅ ) )
3	1 2	syl	⊢ ( 𝐴 = if ( 𝐴 ∈ On , 𝐴 , ∅ ) → suc suc 𝐴 = suc suc if ( 𝐴 ∈ On , 𝐴 , ∅ ) )
4	3	eleq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ On , 𝐴 , ∅ ) → ( suc suc 𝐴 ∈ Comp ↔ suc suc if ( 𝐴 ∈ On , 𝐴 , ∅ ) ∈ Comp ) )
5		0elon	⊢ ∅ ∈ On
6	5	elimel	⊢ if ( 𝐴 ∈ On , 𝐴 , ∅ ) ∈ On
7	6	onsucsuccmpi	⊢ suc suc if ( 𝐴 ∈ On , 𝐴 , ∅ ) ∈ Comp
8	4 7	dedth	⊢ ( 𝐴 ∈ On → suc suc 𝐴 ∈ Comp )