Theorem onsucconn

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

	Ref	Expression
Assertion	onsucconn	$$⊢A\in \mathrm{On}\to \mathrm{suc}A\in \mathrm{Conn}$$

Proof

Step	Hyp	Ref	Expression
1		suceq	$$⊢A=if\left(A\in \mathrm{On},A,\varnothing \right)\to \mathrm{suc}A=\mathrm{suc}if\left(A\in \mathrm{On},A,\varnothing \right)$$
2	1	eleq1d	$$⊢A=if\left(A\in \mathrm{On},A,\varnothing \right)\to \left(\mathrm{suc}A\in \mathrm{Conn}\leftrightarrow \mathrm{suc}if\left(A\in \mathrm{On},A,\varnothing \right)\in \mathrm{Conn}\right)$$
3		0elon	$$⊢\varnothing \in \mathrm{On}$$
4	3	elimel	$$⊢if\left(A\in \mathrm{On},A,\varnothing \right)\in \mathrm{On}$$
5	4	onsucconni	$$⊢\mathrm{suc}if\left(A\in \mathrm{On},A,\varnothing \right)\in \mathrm{Conn}$$
6	2 5	dedth	$$⊢A\in \mathrm{On}\to \mathrm{suc}A\in \mathrm{Conn}$$