Theorem onsucconn

Description: A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015)

	Ref	Expression
Assertion	onsucconn	|- ( A e. On -> suc A e. Conn )

Proof

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