Description: A successor ordinal number is a topology. (Contributed by Chen-Pang He, 11-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | onsuctop | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ontgsucval | |
|
2 | suceloni | |
|
3 | ontopbas | |
|
4 | tgcl | |
|
5 | 2 3 4 | 3syl | |
6 | 1 5 | eqeltrrd | |