Theorem ontopbas

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

	Ref	Expression
Assertion	ontopbas	|- ( B e. On -> B e. TopBases )

Proof

Step	Hyp	Ref	Expression
1		onelon	|- ( ( B e. On /\ x e. B ) -> x e. On )
2		onelon	|- ( ( B e. On /\ y e. B ) -> y e. On )
3	1 2	anim12dan	|- ( ( B e. On /\ ( x e. B /\ y e. B ) ) -> ( x e. On /\ y e. On ) )
4	3	ex	|- ( B e. On -> ( ( x e. B /\ y e. B ) -> ( x e. On /\ y e. On ) ) )
5		onin	|- ( ( x e. On /\ y e. On ) -> ( x i^i y ) e. On )
6	4 5	syl6	|- ( B e. On -> ( ( x e. B /\ y e. B ) -> ( x i^i y ) e. On ) )
7	6	anc2ri	|- ( B e. On -> ( ( x e. B /\ y e. B ) -> ( ( x i^i y ) e. On /\ B e. On ) ) )
8		inss1	|- ( x i^i y ) C_ x
9	8	jctl	|- ( x e. B -> ( ( x i^i y ) C_ x /\ x e. B ) )
10	9	adantr	|- ( ( x e. B /\ y e. B ) -> ( ( x i^i y ) C_ x /\ x e. B ) )
11	10	a1i	|- ( B e. On -> ( ( x e. B /\ y e. B ) -> ( ( x i^i y ) C_ x /\ x e. B ) ) )
12		ontr2	|- ( ( ( x i^i y ) e. On /\ B e. On ) -> ( ( ( x i^i y ) C_ x /\ x e. B ) -> ( x i^i y ) e. B ) )
13	7 11 12	syl6c	|- ( B e. On -> ( ( x e. B /\ y e. B ) -> ( x i^i y ) e. B ) )
14	13	ralrimivv	|- ( B e. On -> A. x e. B A. y e. B ( x i^i y ) e. B )
15		fiinbas	|- ( ( B e. On /\ A. x e. B A. y e. B ( x i^i y ) e. B ) -> B e. TopBases )
16	14 15	mpdan	|- ( B e. On -> B e. TopBases )