Theorem toponss

Description: A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Assertion	toponss	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge A\in J\right)\to A\subseteq X$$

Proof

Step	Hyp	Ref	Expression
1		elssuni	$$⊢A\in J\to A\subseteq \bigcup J$$
2	1	adantl	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge A\in J\right)\to A\subseteq \bigcup J$$
3		toponuni	$$⊢J\in \mathrm{TopOn}\left(X\right)\to X=\bigcup J$$
4	3	adantr	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge A\in J\right)\to X=\bigcup J$$
5	2 4	sseqtrrd	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge A\in J\right)\to A\subseteq X$$