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 ⊢ Ⅎ 𝑥 𝜑
salpreimaltle.a ⊢ Ⅎ 𝑎 𝜑
salpreimaltle.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
salpreimaltle.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
salpreimaltle.p ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎 } ∈ 𝑆 )
salpreimaltle.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion salpreimaltle ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 salpreimaltle.x ⊢ Ⅎ 𝑥 𝜑
2 salpreimaltle.a ⊢ Ⅎ 𝑎 𝜑
3 salpreimaltle.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4 salpreimaltle.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
5 salpreimaltle.p ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎 } ∈ 𝑆 )
6 salpreimaltle.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
7 1 4 6 preimaleiinlt ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } = ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
8 nnct ⊢ ℕ ≼ ω
9 8 a1i ⊢ ( 𝜑 → ℕ ≼ ω )
10 nnn0 ⊢ ℕ ≠ ∅
11 10 a1i ⊢ ( 𝜑 → ℕ ≠ ∅ )
12 simpl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝜑 )
13 simpl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℝ )
14 nnrecre ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
15 14 adantl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ )
16 13 15 readdcld ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ )
17 6 16 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ )
18 nfv ⊢ Ⅎ 𝑎 ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ
19 2 18 nfan ⊢ Ⅎ 𝑎 ( 𝜑 ∧ ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ )
20 nfv ⊢ Ⅎ 𝑎 { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ∈ 𝑆
21 19 20 nfim ⊢ Ⅎ 𝑎 ( ( 𝜑 ∧ ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ∈ 𝑆 )
22 ovex ⊢ ( 𝐶 + ( 1 / 𝑛 ) ) ∈ V
23 eleq1 ⊢ ( 𝑎 = ( 𝐶 + ( 1 / 𝑛 ) ) → ( 𝑎 ∈ ℝ ↔ ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ ) )
24 23 anbi2d ⊢ ( 𝑎 = ( 𝐶 + ( 1 / 𝑛 ) ) → ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ↔ ( 𝜑 ∧ ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ ) ) )
25 breq2 ⊢ ( 𝑎 = ( 𝐶 + ( 1 / 𝑛 ) ) → ( 𝐵 < 𝑎 ↔ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) )
26 25 rabbidv ⊢ ( 𝑎 = ( 𝐶 + ( 1 / 𝑛 ) ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎 } = { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
27 26 eleq1d ⊢ ( 𝑎 = ( 𝐶 + ( 1 / 𝑛 ) ) → ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎 } ∈ 𝑆 ↔ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ∈ 𝑆 ) )
28 24 27 imbi12d ⊢ ( 𝑎 = ( 𝐶 + ( 1 / 𝑛 ) ) → ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎 } ∈ 𝑆 ) ↔ ( ( 𝜑 ∧ ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ∈ 𝑆 ) ) )
29 21 22 28 5 vtoclf ⊢ ( ( 𝜑 ∧ ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ∈ 𝑆 )
30 12 17 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ∈ 𝑆 )
31 3 9 11 30 saliincl ⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ∈ 𝑆 )
32 7 31 eqeltrd ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } ∈ 𝑆 )