Theorem onsucconni

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

	Ref	Expression
Hypothesis	onsucconni.1	⊢ 𝐴 ∈ On
Assertion	onsucconni	⊢ suc 𝐴 ∈ Conn

Proof

Step	Hyp	Ref	Expression
1		onsucconni.1	⊢ 𝐴 ∈ On
2		onsuctop	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ Top )
3	1 2	ax-mp	⊢ suc 𝐴 ∈ Top
4		elin	⊢ ( 𝑥 ∈ ( suc 𝐴 ∩ ( Clsd ‘ suc 𝐴 ) ) ↔ ( 𝑥 ∈ suc 𝐴 ∧ 𝑥 ∈ ( Clsd ‘ suc 𝐴 ) ) )
5		elsuci	⊢ ( 𝑥 ∈ suc 𝐴 → ( 𝑥 ∈ 𝐴 ∨ 𝑥 = 𝐴 ) )
6	1	onunisuci	⊢ ∪ suc 𝐴 = 𝐴
7	6	eqcomi	⊢ 𝐴 = ∪ suc 𝐴
8	7	cldopn	⊢ ( 𝑥 ∈ ( Clsd ‘ suc 𝐴 ) → ( 𝐴 ∖ 𝑥 ) ∈ suc 𝐴 )
9	1	onsuci	⊢ suc 𝐴 ∈ On
10	9	oneli	⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ suc 𝐴 → ( 𝐴 ∖ 𝑥 ) ∈ On )
11		elndif	⊢ ( ∅ ∈ 𝑥 → ¬ ∅ ∈ ( 𝐴 ∖ 𝑥 ) )
12		on0eln0	⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ On → ( ∅ ∈ ( 𝐴 ∖ 𝑥 ) ↔ ( 𝐴 ∖ 𝑥 ) ≠ ∅ ) )
13	12	biimprd	⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ On → ( ( 𝐴 ∖ 𝑥 ) ≠ ∅ → ∅ ∈ ( 𝐴 ∖ 𝑥 ) ) )
14	13	necon1bd	⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ On → ( ¬ ∅ ∈ ( 𝐴 ∖ 𝑥 ) → ( 𝐴 ∖ 𝑥 ) = ∅ ) )
15		ssdif0	⊢ ( 𝐴 ⊆ 𝑥 ↔ ( 𝐴 ∖ 𝑥 ) = ∅ )
16	1	onssneli	⊢ ( 𝐴 ⊆ 𝑥 → ¬ 𝑥 ∈ 𝐴 )
17	15 16	sylbir	⊢ ( ( 𝐴 ∖ 𝑥 ) = ∅ → ¬ 𝑥 ∈ 𝐴 )
18	11 14 17	syl56	⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ On → ( ∅ ∈ 𝑥 → ¬ 𝑥 ∈ 𝐴 ) )
19	18	con2d	⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ On → ( 𝑥 ∈ 𝐴 → ¬ ∅ ∈ 𝑥 ) )
20	1	oneli	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ On )
21		on0eln0	⊢ ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 ↔ 𝑥 ≠ ∅ ) )
22	21	biimprd	⊢ ( 𝑥 ∈ On → ( 𝑥 ≠ ∅ → ∅ ∈ 𝑥 ) )
23	20 22	syl	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ≠ ∅ → ∅ ∈ 𝑥 ) )
24	23	necon1bd	⊢ ( 𝑥 ∈ 𝐴 → ( ¬ ∅ ∈ 𝑥 → 𝑥 = ∅ ) )
25	19 24	sylcom	⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ On → ( 𝑥 ∈ 𝐴 → 𝑥 = ∅ ) )
26	10 25	syl	⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ suc 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 = ∅ ) )
27	26	orim1d	⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ suc 𝐴 → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 = 𝐴 ) → ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) )
28	27	impcom	⊢ ( ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 = 𝐴 ) ∧ ( 𝐴 ∖ 𝑥 ) ∈ suc 𝐴 ) → ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) )
29		vex	⊢ 𝑥 ∈ V
30	29	elpr	⊢ ( 𝑥 ∈ { ∅ , 𝐴 } ↔ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) )
31	28 30	sylibr	⊢ ( ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 = 𝐴 ) ∧ ( 𝐴 ∖ 𝑥 ) ∈ suc 𝐴 ) → 𝑥 ∈ { ∅ , 𝐴 } )
32	5 8 31	syl2an	⊢ ( ( 𝑥 ∈ suc 𝐴 ∧ 𝑥 ∈ ( Clsd ‘ suc 𝐴 ) ) → 𝑥 ∈ { ∅ , 𝐴 } )
33	4 32	sylbi	⊢ ( 𝑥 ∈ ( suc 𝐴 ∩ ( Clsd ‘ suc 𝐴 ) ) → 𝑥 ∈ { ∅ , 𝐴 } )
34	33	ssriv	⊢ ( suc 𝐴 ∩ ( Clsd ‘ suc 𝐴 ) ) ⊆ { ∅ , 𝐴 }
35	7	isconn2	⊢ ( suc 𝐴 ∈ Conn ↔ ( suc 𝐴 ∈ Top ∧ ( suc 𝐴 ∩ ( Clsd ‘ suc 𝐴 ) ) ⊆ { ∅ , 𝐴 } ) )
36	3 34 35	mpbir2an	⊢ suc 𝐴 ∈ Conn