ontopbas

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

		Ref	Expression
	Assertion	ontopbas	$⊢ B \in On \to B \in TopBases$

Step	Hyp	Ref	Expression
1		onelon	$⊢ (B \in On \land x \in B) \to x \in On$
2		onelon	$⊢ (B \in On \land y \in B) \to y \in On$
3	1 2	anim12dan	$⊢ (B \in On \land (x \in B \land y \in B)) \to (x \in On \land y \in On)$
4	3	ex	$⊢ B \in On \to ((x \in B \land y \in B) \to (x \in On \land y \in On))$
5		onin	$⊢ (x \in On \land y \in On) \to x \cap y \in On$
6	4 5	syl6	$⊢ B \in On \to ((x \in B \land y \in B) \to x \cap y \in On)$
7	6	anc2ri	$⊢ B \in On \to ((x \in B \land y \in B) \to (x \cap y \in On \land B \in On))$
8		inss1	$⊢ x \cap y \subseteq x$
9	8	jctl	$⊢ x \in B \to (x \cap y \subseteq x \land x \in B)$
10	9	adantr	$⊢ (x \in B \land y \in B) \to (x \cap y \subseteq x \land x \in B)$
11	10	a1i	$⊢ B \in On \to ((x \in B \land y \in B) \to (x \cap y \subseteq x \land x \in B))$
12		ontr2	$⊢ (x \cap y \in On \land B \in On) \to ((x \cap y \subseteq x \land x \in B) \to x \cap y \in B)$
13	7 11 12	syl6c	$⊢ B \in On \to ((x \in B \land y \in B) \to x \cap y \in B)$
14	13	ralrimivv	$⊢ B \in On \to \forall x \in B \forall y \in B x \cap y \in B$
15		fiinbas	$⊢ (B \in On \land \forall x \in B \forall y \in B x \cap y \in B) \to B \in TopBases$
16	14 15	mpdan	$⊢ B \in On \to B \in TopBases$

Metamath Proof Explorer