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 ( 𝐵 ∈ On → 𝐵 ∈ TopBases )

Proof

Step Hyp Ref Expression
1 onelon ( ( 𝐵 ∈ On ∧ 𝑥𝐵 ) → 𝑥 ∈ On )
2 onelon ( ( 𝐵 ∈ On ∧ 𝑦𝐵 ) → 𝑦 ∈ On )
3 1 2 anim12dan ( ( 𝐵 ∈ On ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) )
4 3 ex ( 𝐵 ∈ On → ( ( 𝑥𝐵𝑦𝐵 ) → ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) )
5 onin ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥𝑦 ) ∈ On )
6 4 5 syl6 ( 𝐵 ∈ On → ( ( 𝑥𝐵𝑦𝐵 ) → ( 𝑥𝑦 ) ∈ On ) )
7 6 anc2ri ( 𝐵 ∈ On → ( ( 𝑥𝐵𝑦𝐵 ) → ( ( 𝑥𝑦 ) ∈ On ∧ 𝐵 ∈ On ) ) )
8 inss1 ( 𝑥𝑦 ) ⊆ 𝑥
9 8 jctl ( 𝑥𝐵 → ( ( 𝑥𝑦 ) ⊆ 𝑥𝑥𝐵 ) )
10 9 adantr ( ( 𝑥𝐵𝑦𝐵 ) → ( ( 𝑥𝑦 ) ⊆ 𝑥𝑥𝐵 ) )
11 10 a1i ( 𝐵 ∈ On → ( ( 𝑥𝐵𝑦𝐵 ) → ( ( 𝑥𝑦 ) ⊆ 𝑥𝑥𝐵 ) ) )
12 ontr2 ( ( ( 𝑥𝑦 ) ∈ On ∧ 𝐵 ∈ On ) → ( ( ( 𝑥𝑦 ) ⊆ 𝑥𝑥𝐵 ) → ( 𝑥𝑦 ) ∈ 𝐵 ) )
13 7 11 12 syl6c ( 𝐵 ∈ On → ( ( 𝑥𝐵𝑦𝐵 ) → ( 𝑥𝑦 ) ∈ 𝐵 ) )
14 13 ralrimivv ( 𝐵 ∈ On → ∀ 𝑥𝐵𝑦𝐵 ( 𝑥𝑦 ) ∈ 𝐵 )
15 fiinbas ( ( 𝐵 ∈ On ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥𝑦 ) ∈ 𝐵 ) → 𝐵 ∈ TopBases )
16 14 15 mpdan ( 𝐵 ∈ On → 𝐵 ∈ TopBases )