Metamath Proof Explorer


Theorem incsmf

Description: A real-valued, nondecreasing function is Borel measurable. Proposition 121D (c) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses incsmf.a ( 𝜑𝐴 ⊆ ℝ )
incsmf.f ( 𝜑𝐹 : 𝐴 ⟶ ℝ )
incsmf.i ( 𝜑 → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 → ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) ) )
incsmf.j 𝐽 = ( topGen ‘ ran (,) )
incsmf.b 𝐵 = ( SalGen ‘ 𝐽 )
Assertion incsmf ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 incsmf.a ( 𝜑𝐴 ⊆ ℝ )
2 incsmf.f ( 𝜑𝐹 : 𝐴 ⟶ ℝ )
3 incsmf.i ( 𝜑 → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 → ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) ) )
4 incsmf.j 𝐽 = ( topGen ‘ ran (,) )
5 incsmf.b 𝐵 = ( SalGen ‘ 𝐽 )
6 nfv 𝑎 𝜑
7 retop ( topGen ‘ ran (,) ) ∈ Top
8 4 7 eqeltri 𝐽 ∈ Top
9 8 a1i ( 𝜑𝐽 ∈ Top )
10 9 5 salgencld ( 𝜑𝐵 ∈ SAlg )
11 9 5 unisalgen2 ( 𝜑 𝐵 = 𝐽 )
12 4 unieqi 𝐽 = ( topGen ‘ ran (,) )
13 12 a1i ( 𝜑 𝐽 = ( topGen ‘ ran (,) ) )
14 uniretop ℝ = ( topGen ‘ ran (,) )
15 14 eqcomi ( topGen ‘ ran (,) ) = ℝ
16 15 a1i ( 𝜑 ( topGen ‘ ran (,) ) = ℝ )
17 11 13 16 3eqtrrd ( 𝜑 → ℝ = 𝐵 )
18 1 17 sseqtrd ( 𝜑𝐴 𝐵 )
19 nfv 𝑤 ( 𝜑𝑎 ∈ ℝ )
20 nfv 𝑧 ( 𝜑𝑎 ∈ ℝ )
21 1 adantr ( ( 𝜑𝑎 ∈ ℝ ) → 𝐴 ⊆ ℝ )
22 2 frexr ( 𝜑𝐹 : 𝐴 ⟶ ℝ* )
23 22 adantr ( ( 𝜑𝑎 ∈ ℝ ) → 𝐹 : 𝐴 ⟶ ℝ* )
24 breq1 ( 𝑥 = 𝑤 → ( 𝑥𝑦𝑤𝑦 ) )
25 fveq2 ( 𝑥 = 𝑤 → ( 𝐹𝑥 ) = ( 𝐹𝑤 ) )
26 25 breq1d ( 𝑥 = 𝑤 → ( ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) ↔ ( 𝐹𝑤 ) ≤ ( 𝐹𝑦 ) ) )
27 24 26 imbi12d ( 𝑥 = 𝑤 → ( ( 𝑥𝑦 → ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) ) ↔ ( 𝑤𝑦 → ( 𝐹𝑤 ) ≤ ( 𝐹𝑦 ) ) ) )
28 breq2 ( 𝑦 = 𝑧 → ( 𝑤𝑦𝑤𝑧 ) )
29 fveq2 ( 𝑦 = 𝑧 → ( 𝐹𝑦 ) = ( 𝐹𝑧 ) )
30 29 breq2d ( 𝑦 = 𝑧 → ( ( 𝐹𝑤 ) ≤ ( 𝐹𝑦 ) ↔ ( 𝐹𝑤 ) ≤ ( 𝐹𝑧 ) ) )
31 28 30 imbi12d ( 𝑦 = 𝑧 → ( ( 𝑤𝑦 → ( 𝐹𝑤 ) ≤ ( 𝐹𝑦 ) ) ↔ ( 𝑤𝑧 → ( 𝐹𝑤 ) ≤ ( 𝐹𝑧 ) ) ) )
32 27 31 cbvral2vw ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 → ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) ) ↔ ∀ 𝑤𝐴𝑧𝐴 ( 𝑤𝑧 → ( 𝐹𝑤 ) ≤ ( 𝐹𝑧 ) ) )
33 3 32 sylib ( 𝜑 → ∀ 𝑤𝐴𝑧𝐴 ( 𝑤𝑧 → ( 𝐹𝑤 ) ≤ ( 𝐹𝑧 ) ) )
34 33 adantr ( ( 𝜑𝑎 ∈ ℝ ) → ∀ 𝑤𝐴𝑧𝐴 ( 𝑤𝑧 → ( 𝐹𝑤 ) ≤ ( 𝐹𝑧 ) ) )
35 rexr ( 𝑎 ∈ ℝ → 𝑎 ∈ ℝ* )
36 35 adantl ( ( 𝜑𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ* )
37 25 breq1d ( 𝑥 = 𝑤 → ( ( 𝐹𝑥 ) < 𝑎 ↔ ( 𝐹𝑤 ) < 𝑎 ) )
38 37 cbvrabv { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } = { 𝑤𝐴 ∣ ( 𝐹𝑤 ) < 𝑎 }
39 eqid sup ( { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } , ℝ* , < ) = sup ( { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } , ℝ* , < )
40 eqid ( -∞ (,) sup ( { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } , ℝ* , < ) ) = ( -∞ (,) sup ( { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } , ℝ* , < ) )
41 eqid ( -∞ (,] sup ( { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } , ℝ* , < ) ) = ( -∞ (,] sup ( { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } , ℝ* , < ) )
42 19 20 21 23 34 4 5 36 38 39 40 41 incsmflem ( ( 𝜑𝑎 ∈ ℝ ) → ∃ 𝑏𝐵 { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } = ( 𝑏𝐴 ) )
43 reex ℝ ∈ V
44 43 a1i ( 𝜑 → ℝ ∈ V )
45 44 1 ssexd ( 𝜑𝐴 ∈ V )
46 elrest ( ( 𝐵 ∈ SAlg ∧ 𝐴 ∈ V ) → ( { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } ∈ ( 𝐵t 𝐴 ) ↔ ∃ 𝑏𝐵 { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } = ( 𝑏𝐴 ) ) )
47 10 45 46 syl2anc ( 𝜑 → ( { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } ∈ ( 𝐵t 𝐴 ) ↔ ∃ 𝑏𝐵 { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } = ( 𝑏𝐴 ) ) )
48 47 adantr ( ( 𝜑𝑎 ∈ ℝ ) → ( { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } ∈ ( 𝐵t 𝐴 ) ↔ ∃ 𝑏𝐵 { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } = ( 𝑏𝐴 ) ) )
49 42 48 mpbird ( ( 𝜑𝑎 ∈ ℝ ) → { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝑎 } ∈ ( 𝐵t 𝐴 ) )
50 6 10 18 2 49 issmfd ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝐵 ) )