Theorem baspartn

Description: A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Assertion	baspartn	$$⊢\left(P\in V\wedge \forall x\in P\forall y\in P\left(x=y\vee x\cap y=\varnothing \right)\right)\to P\in \mathrm{TopBases}$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢x\in P\to x\in P$$
2		pwidg	$$⊢x\in P\to x\in 𝒫x$$
3	1 2	elind	$$⊢x\in P\to x\in \left(P\cap 𝒫x\right)$$
4		elssuni	$$⊢x\in \left(P\cap 𝒫x\right)\to x\subseteq \bigcup \left(P\cap 𝒫x\right)$$
5	3 4	syl	$$⊢x\in P\to x\subseteq \bigcup \left(P\cap 𝒫x\right)$$
6		inidm	$$⊢x\cap x=x$$
7		ineq2	$$⊢x=y\to x\cap x=x\cap y$$
8	6 7	eqtr3id	$$⊢x=y\to x=x\cap y$$
9	8	pweqd	$$⊢x=y\to 𝒫x=𝒫\left(x\cap y\right)$$
10	9	ineq2d	$$⊢x=y\to P\cap 𝒫x=P\cap 𝒫\left(x\cap y\right)$$
11	10	unieqd	$$⊢x=y\to \bigcup \left(P\cap 𝒫x\right)=\bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)$$
12	8 11	sseq12d	$$⊢x=y\to \left(x\subseteq \bigcup \left(P\cap 𝒫x\right)\leftrightarrow x\cap y\subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)\right)$$
13	5 12	syl5ibcom	$$⊢x\in P\to \left(x=y\to x\cap y\subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)\right)$$
14		0ss	$$⊢\varnothing \subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)$$
15		sseq1	$$⊢x\cap y=\varnothing \to \left(x\cap y\subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)\leftrightarrow \varnothing \subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)\right)$$
16	14 15	mpbiri	$$⊢x\cap y=\varnothing \to x\cap y\subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)$$
17	16	a1i	$$⊢x\in P\to \left(x\cap y=\varnothing \to x\cap y\subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)\right)$$
18	13 17	jaod	$$⊢x\in P\to \left(\left(x=y\vee x\cap y=\varnothing \right)\to x\cap y\subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)\right)$$
19	18	ralimdv	$$⊢x\in P\to \left(\forall y\in P\left(x=y\vee x\cap y=\varnothing \right)\to \forall y\in Px\cap y\subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)\right)$$
20	19	ralimia	$$⊢\forall x\in P\forall y\in P\left(x=y\vee x\cap y=\varnothing \right)\to \forall x\in P\forall y\in Px\cap y\subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)$$
21	20	adantl	$$⊢\left(P\in V\wedge \forall x\in P\forall y\in P\left(x=y\vee x\cap y=\varnothing \right)\right)\to \forall x\in P\forall y\in Px\cap y\subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)$$
22		isbasisg	$$⊢P\in V\to \left(P\in \mathrm{TopBases}\leftrightarrow \forall x\in P\forall y\in Px\cap y\subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)\right)$$
23	22	adantr	$$⊢\left(P\in V\wedge \forall x\in P\forall y\in P\left(x=y\vee x\cap y=\varnothing \right)\right)\to \left(P\in \mathrm{TopBases}\leftrightarrow \forall x\in P\forall y\in Px\cap y\subseteq \bigcup \left(P\cap 𝒫\left(x\cap y\right)\right)\right)$$
24	21 23	mpbird	$$⊢\left(P\in V\wedge \forall x\in P\forall y\in P\left(x=y\vee x\cap y=\varnothing \right)\right)\to P\in \mathrm{TopBases}$$