Theorem iocborel

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

	Ref	Expression
Hypotheses	iocborel.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	iocborel.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	iocborel.t	⊢ 𝐽 = ( topGen ‘ ran (,) )
	iocborel.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
Assertion	iocborel	⊢ ( 𝜑 → ( 𝐴 (,] 𝐶 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		iocborel.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		iocborel.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3		iocborel.t	⊢ 𝐽 = ( topGen ‘ ran (,) )
4		iocborel.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
5	1 2	iooiinioc	⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ ( 𝐴 (,) ( 𝐶 + ( 1 / 𝑛 ) ) ) = ( 𝐴 (,] 𝐶 ) )
6	5	eqcomd	⊢ ( 𝜑 → ( 𝐴 (,] 𝐶 ) = ∩ 𝑛 ∈ ℕ ( 𝐴 (,) ( 𝐶 + ( 1 / 𝑛 ) ) ) )
7	3 4	bor1sal	⊢ 𝐵 ∈ SAlg
8	7	a1i	⊢ ( ⊤ → 𝐵 ∈ SAlg )
9		nnct	⊢ ℕ ≼ ω
10	9	a1i	⊢ ( ⊤ → ℕ ≼ ω )
11		nnn0	⊢ ℕ ≠ ∅
12	11	a1i	⊢ ( ⊤ → ℕ ≠ ∅ )
13	3 4	iooborel	⊢ ( 𝐴 (,) ( 𝐶 + ( 1 / 𝑛 ) ) ) ∈ 𝐵
14	13	a1i	⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( 𝐴 (,) ( 𝐶 + ( 1 / 𝑛 ) ) ) ∈ 𝐵 )
15	8 10 12 14	saliincl	⊢ ( ⊤ → ∩ 𝑛 ∈ ℕ ( 𝐴 (,) ( 𝐶 + ( 1 / 𝑛 ) ) ) ∈ 𝐵 )
16	15	mptru	⊢ ∩ 𝑛 ∈ ℕ ( 𝐴 (,) ( 𝐶 + ( 1 / 𝑛 ) ) ) ∈ 𝐵
17	16	a1i	⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ ( 𝐴 (,) ( 𝐶 + ( 1 / 𝑛 ) ) ) ∈ 𝐵 )
18	6 17	eqeltrd	⊢ ( 𝜑 → ( 𝐴 (,] 𝐶 ) ∈ 𝐵 )