Theorem toponunii

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

	Ref	Expression
Hypothesis	topontopi.1	⊢ 𝐽 ∈ ( TopOn ‘ 𝐵 )
Assertion	toponunii	⊢ 𝐵 = ∪ 𝐽

Proof

Step	Hyp	Ref	Expression
1		topontopi.1	⊢ 𝐽 ∈ ( TopOn ‘ 𝐵 )
2		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 = ∪ 𝐽 )
3	1 2	ax-mp	⊢ 𝐵 = ∪ 𝐽