Theorem bastop1

Description: A subset of a topology is a basis for the topology iff every member of the topology is a union of members of the basis. We use the idiom " ( topGenB ) = J " to express " B is a basis for topology J " since we do not have a separate notation for this. Definition 15.35 of Schechter p. 428. (Contributed by NM, 2-Feb-2008) (Proof shortened by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Assertion	bastop1	$$⊢\left(J\in \mathrm{Top}\wedge B\subseteq J\right)\to \left(\mathrm{topGen}\left(B\right)=J\leftrightarrow \forall x\in J\exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		tgss	$$⊢\left(J\in \mathrm{Top}\wedge B\subseteq J\right)\to \mathrm{topGen}\left(B\right)\subseteq \mathrm{topGen}\left(J\right)$$
2		tgtop	$$⊢J\in \mathrm{Top}\to \mathrm{topGen}\left(J\right)=J$$
3	2	adantr	$$⊢\left(J\in \mathrm{Top}\wedge B\subseteq J\right)\to \mathrm{topGen}\left(J\right)=J$$
4	1 3	sseqtrd	$$⊢\left(J\in \mathrm{Top}\wedge B\subseteq J\right)\to \mathrm{topGen}\left(B\right)\subseteq J$$
5		eqss	$$⊢\mathrm{topGen}\left(B\right)=J\leftrightarrow \left(\mathrm{topGen}\left(B\right)\subseteq J\wedge J\subseteq \mathrm{topGen}\left(B\right)\right)$$
6	5	baib	$$⊢\mathrm{topGen}\left(B\right)\subseteq J\to \left(\mathrm{topGen}\left(B\right)=J\leftrightarrow J\subseteq \mathrm{topGen}\left(B\right)\right)$$
7	4 6	syl	$$⊢\left(J\in \mathrm{Top}\wedge B\subseteq J\right)\to \left(\mathrm{topGen}\left(B\right)=J\leftrightarrow J\subseteq \mathrm{topGen}\left(B\right)\right)$$
8		dfss3	$$⊢J\subseteq \mathrm{topGen}\left(B\right)\leftrightarrow \forall x\in Jx\in \mathrm{topGen}\left(B\right)$$
9	7 8	bitrdi	$$⊢\left(J\in \mathrm{Top}\wedge B\subseteq J\right)\to \left(\mathrm{topGen}\left(B\right)=J\leftrightarrow \forall x\in Jx\in \mathrm{topGen}\left(B\right)\right)$$
10		ssexg	$$⊢\left(B\subseteq J\wedge J\in \mathrm{Top}\right)\to B\in \mathrm{V}$$
11	10	ancoms	$$⊢\left(J\in \mathrm{Top}\wedge B\subseteq J\right)\to B\in \mathrm{V}$$
12		eltg3	$$⊢B\in \mathrm{V}\to \left(x\in \mathrm{topGen}\left(B\right)\leftrightarrow \exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right)$$
13	11 12	syl	$$⊢\left(J\in \mathrm{Top}\wedge B\subseteq J\right)\to \left(x\in \mathrm{topGen}\left(B\right)\leftrightarrow \exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right)$$
14	13	ralbidv	$$⊢\left(J\in \mathrm{Top}\wedge B\subseteq J\right)\to \left(\forall x\in Jx\in \mathrm{topGen}\left(B\right)\leftrightarrow \forall x\in J\exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right)$$
15	9 14	bitrd	$$⊢\left(J\in \mathrm{Top}\wedge B\subseteq J\right)\to \left(\mathrm{topGen}\left(B\right)=J\leftrightarrow \forall x\in J\exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right)$$