Metamath Proof Explorer

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 ∈ On
Assertion onsucconni ⊢ suc ⁡ A ∈ Conn

Proof

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