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	|- ( A e. On -> suc suc A e. Comp )

Proof

Step	Hyp	Ref	Expression
1		suceq	|- ( A = if ( A e. On , A , (/) ) -> suc A = suc if ( A e. On , A , (/) ) )
2		suceq	|- ( suc A = suc if ( A e. On , A , (/) ) -> suc suc A = suc suc if ( A e. On , A , (/) ) )
3	1 2	syl	|- ( A = if ( A e. On , A , (/) ) -> suc suc A = suc suc if ( A e. On , A , (/) ) )
4	3	eleq1d	|- ( A = if ( A e. On , A , (/) ) -> ( suc suc A e. Comp <-> suc suc if ( A e. On , A , (/) ) e. Comp ) )
5		0elon	|- (/) e. On
6	5	elimel	|- if ( A e. On , A , (/) ) e. On
7	6	onsucsuccmpi	|- suc suc if ( A e. On , A , (/) ) e. Comp
8	4 7	dedth	|- ( A e. On -> suc suc A e. Comp )