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−1n<B
8 nnct ⊢ℕ≼ω
9 8 a1i ⊢φ→ℕ≼ω
10 nnn0 ⊢ℕ≠∅
11 10 a1i ⊢φ→ℕ≠∅
12 6 adantr ⊢φ∧n∈ℕ→C∈ℝ
13 nnrecre ⊢n∈ℕ→1n∈ℝ
14 13 adantl ⊢φ∧n∈ℕ→1n∈ℝ
15 12 14 resubcld ⊢φ∧n∈ℕ→C−1n∈ℝ
16 nfv ⊢ℲaC−1n∈ℝ
17 2 16 nfan ⊢Ⅎaφ∧C−1n∈ℝ
18 nfv ⊢Ⅎax∈A|C−1n<B∈S
19 17 18 nfim ⊢Ⅎaφ∧C−1n∈ℝ→x∈A|C−1n<B∈S
20 ovex ⊢C−1n∈V
21 eleq1 ⊢a=C−1n→a∈ℝ↔C−1n∈ℝ
22 21 anbi2d ⊢a=C−1n→φ∧a∈ℝ↔φ∧C−1n∈ℝ
23 breq1 ⊢a=C−1n→a<B↔C−1n<B
24 23 rabbidv ⊢a=C−1n→x∈A|a<B=x∈A|C−1n<B
25 24 eleq1d ⊢a=C−1n→x∈A|a<B∈S↔x∈A|C−1n<B∈S
26 22 25 imbi12d ⊢a=C−1n→φ∧a∈ℝ→x∈A|a<B∈S↔φ∧C−1n∈ℝ→x∈A|C−1n<B∈S
27 19 20 26 5 vtoclf ⊢φ∧C−1n∈ℝ→x∈A|C−1n<B∈S
28 15 27 syldan ⊢φ∧n∈ℕ→x∈A|C−1n<B∈S
29 3 9 11 28 saliincl ⊢φ→⋂n∈ℕx∈A|C−1n<B∈S
30 7 29 eqeltrd ⊢φ→x∈A|C≤B∈S