Theorem tgfiss

Description: If a subbase is included into a topology, so is the generated topology. (Contributed by FL, 20-Apr-2012) (Proof shortened by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Assertion	tgfiss	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq J\right)\to \mathrm{topGen}\left(\mathrm{fi}\left(A\right)\right)\subseteq J$$

Proof

Step	Hyp	Ref	Expression
1		fiss	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq J\right)\to \mathrm{fi}\left(A\right)\subseteq \mathrm{fi}\left(J\right)$$
2		fitop	$$⊢J\in \mathrm{Top}\to \mathrm{fi}\left(J\right)=J$$
3	2	adantr	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq J\right)\to \mathrm{fi}\left(J\right)=J$$
4	1 3	sseqtrd	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq J\right)\to \mathrm{fi}\left(A\right)\subseteq J$$
5		tgss	$$⊢\left(J\in \mathrm{Top}\wedge \mathrm{fi}\left(A\right)\subseteq J\right)\to \mathrm{topGen}\left(\mathrm{fi}\left(A\right)\right)\subseteq \mathrm{topGen}\left(J\right)$$
6	4 5	syldan	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq J\right)\to \mathrm{topGen}\left(\mathrm{fi}\left(A\right)\right)\subseteq \mathrm{topGen}\left(J\right)$$
7		tgtop	$$⊢J\in \mathrm{Top}\to \mathrm{topGen}\left(J\right)=J$$
8	7	adantr	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq J\right)\to \mathrm{topGen}\left(J\right)=J$$
9	6 8	sseqtrd	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq J\right)\to \mathrm{topGen}\left(\mathrm{fi}\left(A\right)\right)\subseteq J$$