Metamath Proof Explorer

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 ⊢ φ → A ∈ ℝ *
iocborel.c ⊢ φ → C ∈ ℝ
iocborel.t ⊢ J = topGen ⁡ ran ⁡ .
iocborel.b ⊢ B = SalGen ⁡ J
Assertion iocborel ⊢ φ → A C ∈ B

Proof

Step Hyp Ref Expression
1 iocborel.a ⊢ φ → A ∈ ℝ *
2 iocborel.c ⊢ φ → C ∈ ℝ
3 iocborel.t ⊢ J = topGen ⁡ ran ⁡ .
4 iocborel.b ⊢ B = SalGen ⁡ J
5 1 2 iooiinioc ⊢ φ → ⋂ n ∈ ℕ A C + 1 n = A C
6 5 eqcomd ⊢ φ → A C = ⋂ n ∈ ℕ A C + 1 n
7 3 4 bor1sal ⊢ B ∈ SAlg
8 7 a1i ⊢ ⊤ → B ∈ SAlg
9 nnct ⊢ ℕ ≼ ω
10 9 a1i ⊢ ⊤ → ℕ ≼ ω
11 nnn0 ⊢ ℕ ≠ ∅
12 11 a1i ⊢ ⊤ → ℕ ≠ ∅
13 3 4 iooborel ⊢ A C + 1 n ∈ B
14 13 a1i ⊢ ⊤ ∧ n ∈ ℕ → A C + 1 n ∈ B
15 8 10 12 14 saliincl ⊢ ⊤ → ⋂ n ∈ ℕ A C + 1 n ∈ B
16 15 mptru ⊢ ⋂ n ∈ ℕ A C + 1 n ∈ B
17 16 a1i ⊢ φ → ⋂ n ∈ ℕ A C + 1 n ∈ B
18 6 17 eqeltrd ⊢ φ → A C ∈ B