basis1

		Ref	Expression
	Assertion	basis1	$⊢ (B \in TopBases \land C \in B \land D \in B) \to C \cap D \subseteq ⋃ (B \cap 𝒫 (C \cap D))$

Step	Hyp	Ref	Expression
1		isbasisg	$⊢ B \in TopBases \to (B \in TopBases \leftrightarrow \forall x \in B \forall y \in B x \cap y \subseteq ⋃ (B \cap 𝒫 (x \cap y)))$
2	1	ibi	$⊢ B \in TopBases \to \forall x \in B \forall y \in B x \cap y \subseteq ⋃ (B \cap 𝒫 (x \cap y))$
3		ineq1	$⊢ x = C \to x \cap y = C \cap y$
4	3	pweqd	$⊢ x = C \to 𝒫 (x \cap y) = 𝒫 (C \cap y)$
5	4	ineq2d	$⊢ x = C \to B \cap 𝒫 (x \cap y) = B \cap 𝒫 (C \cap y)$
6	5	unieqd	$⊢ x = C \to ⋃ (B \cap 𝒫 (x \cap y)) = ⋃ (B \cap 𝒫 (C \cap y))$
7	3 6	sseq12d	$⊢ x = C \to (x \cap y \subseteq ⋃ (B \cap 𝒫 (x \cap y)) \leftrightarrow C \cap y \subseteq ⋃ (B \cap 𝒫 (C \cap y)))$
8		ineq2	$⊢ y = D \to C \cap y = C \cap D$
9	8	pweqd	$⊢ y = D \to 𝒫 (C \cap y) = 𝒫 (C \cap D)$
10	9	ineq2d	$⊢ y = D \to B \cap 𝒫 (C \cap y) = B \cap 𝒫 (C \cap D)$
11	10	unieqd	$⊢ y = D \to ⋃ (B \cap 𝒫 (C \cap y)) = ⋃ (B \cap 𝒫 (C \cap D))$
12	8 11	sseq12d	$⊢ y = D \to (C \cap y \subseteq ⋃ (B \cap 𝒫 (C \cap y)) \leftrightarrow C \cap D \subseteq ⋃ (B \cap 𝒫 (C \cap D)))$
13	7 12	rspc2v	$⊢ (C \in B \land D \in B) \to (\forall x \in B \forall y \in B x \cap y \subseteq ⋃ (B \cap 𝒫 (x \cap y)) \to C \cap D \subseteq ⋃ (B \cap 𝒫 (C \cap D)))$
14	2 13	syl5com	$⊢ B \in TopBases \to ((C \in B \land D \in B) \to C \cap D \subseteq ⋃ (B \cap 𝒫 (C \cap D)))$
15	14	3impib	$⊢ (B \in TopBases \land C \in B \land D \in B) \to C \cap D \subseteq ⋃ (B \cap 𝒫 (C \cap D))$

Metamath Proof Explorer