Metamath Proof Explorer

Theorem salpreimalelt

Description: If all the preimages of right-closed, unbounded below intervals, belong to a sigma-algebra, then all the preimages of right-open, unbounded below intervals, belong to the sigma-algebra. (ii) implies (i) in Proposition 121B of Fremlin1 p. 36. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses salpreimalelt.x ⊢ Ⅎ x φ
salpreimalelt.a ⊢ Ⅎ a φ
salpreimalelt.s ⊢ φ → S ∈ SAlg
salpreimalelt.u ⊢ A = ⋃ S
salpreimalelt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ *
salpreimalelt.p ⊢ φ ∧ a ∈ ℝ → x ∈ A | B ≤ a ∈ S
salpreimalelt.c ⊢ φ → C ∈ ℝ
Assertion salpreimalelt ⊢ φ → x ∈ A | B < C ∈ S

Proof

Step Hyp Ref Expression
1 salpreimalelt.x ⊢ Ⅎ x φ
2 salpreimalelt.a ⊢ Ⅎ a φ
3 salpreimalelt.s ⊢ φ → S ∈ SAlg
4 salpreimalelt.u ⊢ A = ⋃ S
5 salpreimalelt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ *
6 salpreimalelt.p ⊢ φ ∧ a ∈ ℝ → x ∈ A | B ≤ a ∈ S
7 salpreimalelt.c ⊢ φ → C ∈ ℝ
8 nfv ⊢ Ⅎ x a ∈ ℝ
9 1 8 nfan ⊢ Ⅎ x φ ∧ a ∈ ℝ
10 nfv ⊢ Ⅎ b φ ∧ a ∈ ℝ
11 3 adantr ⊢ φ ∧ a ∈ ℝ → S ∈ SAlg
12 5 adantlr ⊢ φ ∧ a ∈ ℝ ∧ x ∈ A → B ∈ ℝ *
13 nfv ⊢ Ⅎ x b ∈ ℝ
14 1 13 nfan ⊢ Ⅎ x φ ∧ b ∈ ℝ
15 nfv ⊢ Ⅎ a b ∈ ℝ
16 2 15 nfan ⊢ Ⅎ a φ ∧ b ∈ ℝ
17 3 adantr ⊢ φ ∧ b ∈ ℝ → S ∈ SAlg
18 5 adantlr ⊢ φ ∧ b ∈ ℝ ∧ x ∈ A → B ∈ ℝ *
19 6 adantlr ⊢ φ ∧ b ∈ ℝ ∧ a ∈ ℝ → x ∈ A | B ≤ a ∈ S
20 simpr ⊢ φ ∧ b ∈ ℝ → b ∈ ℝ
21 14 16 17 4 18 19 20 salpreimalegt ⊢ φ ∧ b ∈ ℝ → x ∈ A | b < B ∈ S
22 21 adantlr ⊢ φ ∧ a ∈ ℝ ∧ b ∈ ℝ → x ∈ A | b < B ∈ S
23 simpr ⊢ φ ∧ a ∈ ℝ → a ∈ ℝ
24 9 10 11 12 22 23 salpreimagtge ⊢ φ ∧ a ∈ ℝ → x ∈ A | a ≤ B ∈ S
25 1 2 3 4 5 24 7 salpreimagelt ⊢ φ → x ∈ A | B < C ∈ S