Metamath Proof Explorer

Theorem onsucconn

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

Ref Expression
Assertion onsucconn ⊢ A ∈ On → suc ⁡ A ∈ Conn

Proof

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