Metamath Proof Explorer


Theorem onsuct0

Description: A successor ordinal number is a T_0 space. (Contributed by Chen-Pang He, 8-Nov-2015)

Ref Expression
Assertion onsuct0 A On suc A Kol2

Proof

Step Hyp Ref Expression
1 eloni A On Ord A
2 df-ral o suc A x o y o o o suc A x o y o
3 ordelon Ord A x A x On
4 ordelon Ord A y A y On
5 3 4 anim12dan Ord A x A y A x On y On
6 ordsuc Ord A Ord suc A
7 ordelon Ord suc A o suc A o On
8 7 ex Ord suc A o suc A o On
9 6 8 sylbi Ord A o suc A o On
10 9 adantr Ord A x A y A o suc A o On
11 notbi x o y o ¬ x o ¬ y o
12 ontri1 o On x On o x ¬ x o
13 onsssuc o On x On o x o suc x
14 12 13 bitr3d o On x On ¬ x o o suc x
15 14 adantrr o On x On y On ¬ x o o suc x
16 ontri1 o On y On o y ¬ y o
17 onsssuc o On y On o y o suc y
18 16 17 bitr3d o On y On ¬ y o o suc y
19 18 adantrl o On x On y On ¬ y o o suc y
20 15 19 bibi12d o On x On y On ¬ x o ¬ y o o suc x o suc y
21 20 ancoms x On y On o On ¬ x o ¬ y o o suc x o suc y
22 11 21 syl5bb x On y On o On x o y o o suc x o suc y
23 22 biimpd x On y On o On x o y o o suc x o suc y
24 5 10 23 syl6an Ord A x A y A o suc A x o y o o suc x o suc y
25 24 a2d Ord A x A y A o suc A x o y o o suc A o suc x o suc y
26 ordelss Ord A x A x A
27 ordelord Ord A x A Ord x
28 ordsucsssuc Ord x Ord A x A suc x suc A
29 28 ancoms Ord A Ord x x A suc x suc A
30 27 29 syldan Ord A x A x A suc x suc A
31 26 30 mpbid Ord A x A suc x suc A
32 31 ssneld Ord A x A ¬ o suc A ¬ o suc x
33 32 adantrr Ord A x A y A ¬ o suc A ¬ o suc x
34 ordelss Ord A y A y A
35 ordelord Ord A y A Ord y
36 ordsucsssuc Ord y Ord A y A suc y suc A
37 36 ancoms Ord A Ord y y A suc y suc A
38 35 37 syldan Ord A y A y A suc y suc A
39 34 38 mpbid Ord A y A suc y suc A
40 39 ssneld Ord A y A ¬ o suc A ¬ o suc y
41 40 adantrl Ord A x A y A ¬ o suc A ¬ o suc y
42 33 41 jcad Ord A x A y A ¬ o suc A ¬ o suc x ¬ o suc y
43 pm5.21 ¬ o suc x ¬ o suc y o suc x o suc y
44 42 43 syl6 Ord A x A y A ¬ o suc A o suc x o suc y
45 idd Ord A x A y A o suc x o suc y o suc x o suc y
46 44 45 jad Ord A x A y A o suc A o suc x o suc y o suc x o suc y
47 25 46 syld Ord A x A y A o suc A x o y o o suc x o suc y
48 47 alimdv Ord A x A y A o o suc A x o y o o o suc x o suc y
49 2 48 syl5bi Ord A x A y A o suc A x o y o o o suc x o suc y
50 dfcleq suc x = suc y o o suc x o suc y
51 suc11 x On y On suc x = suc y x = y
52 50 51 bitr3id x On y On o o suc x o suc y x = y
53 5 52 syl Ord A x A y A o o suc x o suc y x = y
54 49 53 sylibd Ord A x A y A o suc A x o y o x = y
55 54 ralrimivva Ord A x A y A o suc A x o y o x = y
56 1 55 syl A On x A y A o suc A x o y o x = y
57 onsuctopon A On suc A TopOn A
58 ist0-2 suc A TopOn A suc A Kol2 x A y A o suc A x o y o x = y
59 57 58 syl A On suc A Kol2 x A y A o suc A x o y o x = y
60 56 59 mpbird A On suc A Kol2