Theorem onsucconn

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

	Ref	Expression
Assertion	onsucconn	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ Conn )

Proof

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