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 )