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	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ) → 𝐴 ⊆ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		elssuni	⊢ ( 𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽 )
2	1	adantl	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ) → 𝐴 ⊆ ∪ 𝐽 )
3		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
4	3	adantr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ) → 𝑋 = ∪ 𝐽 )
5	2 4	sseqtrrd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ) → 𝐴 ⊆ 𝑋 )