Theorem iooborel

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

	Ref	Expression
Hypotheses	iooborel.1	⊢ 𝐽 = ( topGen ‘ ran (,) )
	iooborel.2	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
Assertion	iooborel	⊢ ( 𝐴 (,) 𝐶 ) ∈ 𝐵

Proof

Step	Hyp	Ref	Expression
1		iooborel.1	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		iooborel.2	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
3		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
4	1 3	eqeltri	⊢ 𝐽 ∈ Top
5	2	sssalgen	⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ 𝐵 )
6	4 5	ax-mp	⊢ 𝐽 ⊆ 𝐵
7		iooretop	⊢ ( 𝐴 (,) 𝐶 ) ∈ ( topGen ‘ ran (,) )
8	7 1	eleqtrri	⊢ ( 𝐴 (,) 𝐶 ) ∈ 𝐽
9	6 8	sselii	⊢ ( 𝐴 (,) 𝐶 ) ∈ 𝐵