Theorem iiuni

Description: The base set of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Jan-2014)

	Ref	Expression
Assertion	iiuni	$$⊢\left[0,1\right]=\bigcup \mathrm{II}$$

Proof

Step	Hyp	Ref	Expression
1		iitopon	$$⊢\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$$
2	1	toponunii	$$⊢\left[0,1\right]=\bigcup \mathrm{II}$$