This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iooretop

Description: Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007)

		Ref	Expression
	Assertion	iooretop	$⊢ (A, B) \in topGen (ran (.))$

Step	Hyp	Ref	Expression
1		retopbas	$⊢ ran (.) \in TopBases$
2		bastg	$⊢ ran (.) \in TopBases \to ran (.) \subseteq topGen (ran (.))$
3	1 2	ax-mp	$⊢ ran (.) \subseteq topGen (ran (.))$
4		ioorebas	$⊢ (A, B) \in ran (.)$
5	3 4	sselii	$⊢ (A, B) \in topGen (ran (.))$