isbasisg

Description: Express the predicate "the set B is a basis for a topology". (Contributed by NM, 17-Jul-2006)

		Ref	Expression
	Assertion	isbasisg	$⊢ B \in C \to (B \in TopBases \leftrightarrow \forall x \in B \forall y \in B x \cap y \subseteq ⋃ (B \cap 𝒫 (x \cap y)))$

Step	Hyp	Ref	Expression
1		ineq1	$⊢ z = B \to z \cap 𝒫 (x \cap y) = B \cap 𝒫 (x \cap y)$
2	1	unieqd	$⊢ z = B \to ⋃ (z \cap 𝒫 (x \cap y)) = ⋃ (B \cap 𝒫 (x \cap y))$
3	2	sseq2d	$⊢ z = B \to (x \cap y \subseteq ⋃ (z \cap 𝒫 (x \cap y)) \leftrightarrow x \cap y \subseteq ⋃ (B \cap 𝒫 (x \cap y)))$
4	3	raleqbi1dv	$⊢ z = B \to (\forall y \in z x \cap y \subseteq ⋃ (z \cap 𝒫 (x \cap y)) \leftrightarrow \forall y \in B x \cap y \subseteq ⋃ (B \cap 𝒫 (x \cap y)))$
5	4	raleqbi1dv	$⊢ z = B \to (\forall x \in z \forall y \in z x \cap y \subseteq ⋃ (z \cap 𝒫 (x \cap y)) \leftrightarrow \forall x \in B \forall y \in B x \cap y \subseteq ⋃ (B \cap 𝒫 (x \cap y)))$
6		df-bases	$⊢ TopBases = \{z \| \forall x \in z \forall y \in z x \cap y \subseteq ⋃ (z \cap 𝒫 (x \cap y))\}$
7	5 6	elab2g	$⊢ B \in C \to (B \in TopBases \leftrightarrow \forall x \in B \forall y \in B x \cap y \subseteq ⋃ (B \cap 𝒫 (x \cap y)))$

Metamath Proof Explorer