Theorem tsettps

Description: If the topology component is already correctly truncated, then it forms a topological space (with the topology extractor function coming out the same as the component). (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Hypotheses	tsettps.a	$$⊢A={\mathrm{Base}}_K$$
	tsettps.j	$$⊢J=\mathrm{TopSet}\left(K\right)$$
Assertion	tsettps	$$⊢J\in \mathrm{TopOn}\left(A\right)\to K\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		tsettps.a	$$⊢A={\mathrm{Base}}_K$$
2		tsettps.j	$$⊢J=\mathrm{TopSet}\left(K\right)$$
3	1 2	topontopn	$$⊢J\in \mathrm{TopOn}\left(A\right)\to J=\mathrm{TopOpen}\left(K\right)$$
4		id	$$⊢J\in \mathrm{TopOn}\left(A\right)\to J\in \mathrm{TopOn}\left(A\right)$$
5	3 4	eqeltrrd	$$⊢J\in \mathrm{TopOn}\left(A\right)\to \mathrm{TopOpen}\left(K\right)\in \mathrm{TopOn}\left(A\right)$$
6		eqid	$$⊢\mathrm{TopOpen}\left(K\right)=\mathrm{TopOpen}\left(K\right)$$
7	1 6	istps	$$⊢K\in \mathrm{TopSp}\leftrightarrow \mathrm{TopOpen}\left(K\right)\in \mathrm{TopOn}\left(A\right)$$
8	5 7	sylibr	$$⊢J\in \mathrm{TopOn}\left(A\right)\to K\in \mathrm{TopSp}$$