Theorem basis1

Description: Property of a basis. (Contributed by NM, 16-Jul-2006)

	Ref	Expression
Assertion	basis1	$$⊢\left(B\in \mathrm{TopBases}\wedge C\in B\wedge D\in B\right)\to C\cap D\subseteq \bigcup \left(B\cap 𝒫\left(C\cap D\right)\right)$$

Proof

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