Description: An ordinal number is a topological basis. (Contributed by Chen-Pang He, 8-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ontopbas | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | onelon | |
|
2 | onelon | |
|
3 | 1 2 | anim12dan | |
4 | 3 | ex | |
5 | onin | |
|
6 | 4 5 | syl6 | |
7 | 6 | anc2ri | |
8 | inss1 | |
|
9 | 8 | jctl | |
10 | 9 | adantr | |
11 | 10 | a1i | |
12 | ontr2 | |
|
13 | 7 11 12 | syl6c | |
14 | 13 | ralrimivv | |
15 | fiinbas | |
|
16 | 14 15 | mpdan | |