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