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	⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )

Proof

Step	Hyp	Ref	Expression
1		retopbas	⊢ ran (,) ∈ TopBases
2		bastg	⊢ ( ran (,) ∈ TopBases → ran (,) ⊆ ( topGen ‘ ran (,) ) )
3	1 2	ax-mp	⊢ ran (,) ⊆ ( topGen ‘ ran (,) )
4		ioorebas	⊢ ( 𝐴 (,) 𝐵 ) ∈ ran (,)
5	3 4	sselii	⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )