# Metamath Proof Explorer

## Theorem salpreimaltle

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

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

### Proof

Step Hyp Ref Expression
1 salpreimaltle.x $⊢ Ⅎ x φ$
2 salpreimaltle.a $⊢ Ⅎ a φ$
3 salpreimaltle.s $⊢ φ → S ∈ SAlg$
4 salpreimaltle.b $⊢ φ ∧ x ∈ A → B ∈ ℝ *$
5 salpreimaltle.p $⊢ φ ∧ a ∈ ℝ → x ∈ A | B < a ∈ S$
6 salpreimaltle.c $⊢ φ → C ∈ ℝ$
7 1 4 6 preimaleiinlt $⊢ φ → x ∈ A | B ≤ C = ⋂ n ∈ ℕ x ∈ A | B < C + 1 n$
8 nnct $⊢ ℕ ≼ ω$
9 8 a1i $⊢ φ → ℕ ≼ ω$
10 nnn0 $⊢ ℕ ≠ ∅$
11 10 a1i $⊢ φ → ℕ ≠ ∅$
12 simpl $⊢ φ ∧ n ∈ ℕ → φ$
13 simpl $⊢ C ∈ ℝ ∧ n ∈ ℕ → C ∈ ℝ$
14 nnrecre $⊢ n ∈ ℕ → 1 n ∈ ℝ$
15 14 adantl $⊢ C ∈ ℝ ∧ n ∈ ℕ → 1 n ∈ ℝ$
16 13 15 readdcld $⊢ C ∈ ℝ ∧ n ∈ ℕ → C + 1 n ∈ ℝ$
17 6 16 sylan $⊢ φ ∧ n ∈ ℕ → C + 1 n ∈ ℝ$
18 nfv $⊢ Ⅎ a C + 1 n ∈ ℝ$
19 2 18 nfan $⊢ Ⅎ a φ ∧ C + 1 n ∈ ℝ$
20 nfv $⊢ Ⅎ a x ∈ A | B < C + 1 n ∈ S$
21 19 20 nfim $⊢ Ⅎ a φ ∧ C + 1 n ∈ ℝ → x ∈ A | B < C + 1 n ∈ S$
22 ovex $⊢ C + 1 n ∈ V$
23 eleq1 $⊢ a = C + 1 n → a ∈ ℝ ↔ C + 1 n ∈ ℝ$
24 23 anbi2d $⊢ a = C + 1 n → φ ∧ a ∈ ℝ ↔ φ ∧ C + 1 n ∈ ℝ$
25 breq2 $⊢ a = C + 1 n → B < a ↔ B < C + 1 n$
26 25 rabbidv $⊢ a = C + 1 n → x ∈ A | B < a = x ∈ A | B < C + 1 n$
27 26 eleq1d $⊢ a = C + 1 n → x ∈ A | B < a ∈ S ↔ x ∈ A | B < C + 1 n ∈ S$
28 24 27 imbi12d $⊢ a = C + 1 n → φ ∧ a ∈ ℝ → x ∈ A | B < a ∈ S ↔ φ ∧ C + 1 n ∈ ℝ → x ∈ A | B < C + 1 n ∈ S$
29 21 22 28 5 vtoclf $⊢ φ ∧ C + 1 n ∈ ℝ → x ∈ A | B < C + 1 n ∈ S$
30 12 17 29 syl2anc $⊢ φ ∧ n ∈ ℕ → x ∈ A | B < C + 1 n ∈ S$
31 3 9 11 30 saliincl $⊢ φ → ⋂ n ∈ ℕ x ∈ A | B < C + 1 n ∈ S$
32 7 31 eqeltrd $⊢ φ → x ∈ A | B ≤ C ∈ S$