Theorem eltopss

Description: A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006)

	Ref	Expression
Hypothesis	1open.1	$$⊢X=\bigcup J$$
Assertion	eltopss	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\right)\to A\subseteq X$$

Proof

Step	Hyp	Ref	Expression
1		1open.1	$$⊢X=\bigcup J$$
2		elssuni	$$⊢A\in J\to A\subseteq \bigcup J$$
3	2 1	sseqtrrdi	$$⊢A\in J\to A\subseteq X$$
4	3	adantl	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\right)\to A\subseteq X$$