Metamath Proof Explorer

Theorem salpreimagtge

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

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

Proof

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