Theorem iooborel

Description: An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	iooborel.1	|- J = ( topGen ` ran (,) )
	iooborel.2	|- B = ( SalGen ` J )
Assertion	iooborel	|- ( A (,) C ) e. B

Proof

Step	Hyp	Ref	Expression
1		iooborel.1	|- J = ( topGen ` ran (,) )
2		iooborel.2	|- B = ( SalGen ` J )
3		retop	|- ( topGen ` ran (,) ) e. Top
4	1 3	eqeltri	|- J e. Top
5	2	sssalgen	|- ( J e. Top -> J C_ B )
6	4 5	ax-mp	|- J C_ B
7		iooretop	|- ( A (,) C ) e. ( topGen ` ran (,) )
8	7 1	eleqtrri	|- ( A (,) C ) e. J
9	6 8	sselii	|- ( A (,) C ) e. B