Theorem toponcom

Description: If K is a topology on the base set of topology J , then J is a topology on the base of K . (Contributed by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Assertion	toponcom	$$⊢\left(J\in \mathrm{Top}\wedge K\in \mathrm{TopOn}\left(\bigcup J\right)\right)\to J\in \mathrm{TopOn}\left(\bigcup K\right)$$

Proof

Step	Hyp	Ref	Expression
1		toponuni	$$⊢K\in \mathrm{TopOn}\left(\bigcup J\right)\to \bigcup J=\bigcup K$$
2	1	eqcomd	$$⊢K\in \mathrm{TopOn}\left(\bigcup J\right)\to \bigcup K=\bigcup J$$
3	2	anim2i	$$⊢\left(J\in \mathrm{Top}\wedge K\in \mathrm{TopOn}\left(\bigcup J\right)\right)\to \left(J\in \mathrm{Top}\wedge \bigcup K=\bigcup J\right)$$
4		istopon	$$⊢J\in \mathrm{TopOn}\left(\bigcup K\right)\leftrightarrow \left(J\in \mathrm{Top}\wedge \bigcup K=\bigcup J\right)$$
5	3 4	sylibr	$$⊢\left(J\in \mathrm{Top}\wedge K\in \mathrm{TopOn}\left(\bigcup J\right)\right)\to J\in \mathrm{TopOn}\left(\bigcup K\right)$$