Theorem onsucconni

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

	Ref	Expression
Hypothesis	onsucconni.1	|- A e. On
Assertion	onsucconni	|- suc A e. Conn

Proof

Step	Hyp	Ref	Expression
1		onsucconni.1	|- A e. On
2		onsuctop	|- ( A e. On -> suc A e. Top )
3	1 2	ax-mp	|- suc A e. Top
4		elin	|- ( x e. ( suc A i^i ( Clsd ` suc A ) ) <-> ( x e. suc A /\ x e. ( Clsd ` suc A ) ) )
5		elsuci	|- ( x e. suc A -> ( x e. A \/ x = A ) )
6	1	onunisuci	|- U. suc A = A
7	6	eqcomi	|- A = U. suc A
8	7	cldopn	|- ( x e. ( Clsd ` suc A ) -> ( A \ x ) e. suc A )
9	1	onsuci	|- suc A e. On
10	9	oneli	|- ( ( A \ x ) e. suc A -> ( A \ x ) e. On )
11		elndif	|- ( (/) e. x -> -. (/) e. ( A \ x ) )
12		on0eln0	|- ( ( A \ x ) e. On -> ( (/) e. ( A \ x ) <-> ( A \ x ) =/= (/) ) )
13	12	biimprd	|- ( ( A \ x ) e. On -> ( ( A \ x ) =/= (/) -> (/) e. ( A \ x ) ) )
14	13	necon1bd	|- ( ( A \ x ) e. On -> ( -. (/) e. ( A \ x ) -> ( A \ x ) = (/) ) )
15		ssdif0	|- ( A C_ x <-> ( A \ x ) = (/) )
16	1	onssneli	|- ( A C_ x -> -. x e. A )
17	15 16	sylbir	|- ( ( A \ x ) = (/) -> -. x e. A )
18	11 14 17	syl56	|- ( ( A \ x ) e. On -> ( (/) e. x -> -. x e. A ) )
19	18	con2d	|- ( ( A \ x ) e. On -> ( x e. A -> -. (/) e. x ) )
20	1	oneli	|- ( x e. A -> x e. On )
21		on0eln0	|- ( x e. On -> ( (/) e. x <-> x =/= (/) ) )
22	21	biimprd	|- ( x e. On -> ( x =/= (/) -> (/) e. x ) )
23	20 22	syl	|- ( x e. A -> ( x =/= (/) -> (/) e. x ) )
24	23	necon1bd	|- ( x e. A -> ( -. (/) e. x -> x = (/) ) )
25	19 24	sylcom	|- ( ( A \ x ) e. On -> ( x e. A -> x = (/) ) )
26	10 25	syl	|- ( ( A \ x ) e. suc A -> ( x e. A -> x = (/) ) )
27	26	orim1d	|- ( ( A \ x ) e. suc A -> ( ( x e. A \/ x = A ) -> ( x = (/) \/ x = A ) ) )
28	27	impcom	|- ( ( ( x e. A \/ x = A ) /\ ( A \ x ) e. suc A ) -> ( x = (/) \/ x = A ) )
29		vex	|- x e. _V
30	29	elpr	|- ( x e. { (/) , A } <-> ( x = (/) \/ x = A ) )
31	28 30	sylibr	|- ( ( ( x e. A \/ x = A ) /\ ( A \ x ) e. suc A ) -> x e. { (/) , A } )
32	5 8 31	syl2an	|- ( ( x e. suc A /\ x e. ( Clsd ` suc A ) ) -> x e. { (/) , A } )
33	4 32	sylbi	|- ( x e. ( suc A i^i ( Clsd ` suc A ) ) -> x e. { (/) , A } )
34	33	ssriv	|- ( suc A i^i ( Clsd ` suc A ) ) C_ { (/) , A }
35	7	isconn2	|- ( suc A e. Conn <-> ( suc A e. Top /\ ( suc A i^i ( Clsd ` suc A ) ) C_ { (/) , A } ) )
36	3 34 35	mpbir2an	|- suc A e. Conn