Theorem toponmax

Description: The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	toponmax	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 = ∪ 𝐽 )
2		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐽 ∈ Top )
3		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
4	3	topopn	⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽 )
5	2 4	syl	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → ∪ 𝐽 ∈ 𝐽 )
6	1 5	eqeltrd	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 ∈ 𝐽 )