Metamath Proof Explorer


Theorem ontopbas

Description: An ordinal number is a topological basis. (Contributed by Chen-Pang He, 8-Oct-2015)

Ref Expression
Assertion ontopbas BOnBTopBases

Proof

Step Hyp Ref Expression
1 onelon BOnxBxOn
2 onelon BOnyByOn
3 1 2 anim12dan BOnxByBxOnyOn
4 3 ex BOnxByBxOnyOn
5 onin xOnyOnxyOn
6 4 5 syl6 BOnxByBxyOn
7 6 anc2ri BOnxByBxyOnBOn
8 inss1 xyx
9 8 jctl xBxyxxB
10 9 adantr xByBxyxxB
11 10 a1i BOnxByBxyxxB
12 ontr2 xyOnBOnxyxxBxyB
13 7 11 12 syl6c BOnxByBxyB
14 13 ralrimivv BOnxByBxyB
15 fiinbas BOnxByBxyBBTopBases
16 14 15 mpdan BOnBTopBases