Metamath Proof Explorer

Theorem smfco

Description: The composition of a Borel sigma-measurable function with a sigma-measurable function, is sigma-measurable. Proposition 121E (g) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfco.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smfco.f ⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
smfco.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
smfco.b ⊢ 𝐵 = ( SalGen ‘ 𝐽 )
smfco.h ⊢ ( 𝜑 → 𝐻 ∈ ( SMblFn ‘ 𝐵 ) )
Assertion smfco ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 smfco.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2 smfco.f ⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
3 smfco.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
4 smfco.b ⊢ 𝐵 = ( SalGen ‘ 𝐽 )
5 smfco.h ⊢ ( 𝜑 → 𝐻 ∈ ( SMblFn ‘ 𝐵 ) )
6 nfv ⊢ Ⅎ 𝑎 𝜑
7 cnvimass ⊢ ( ◡ 𝐹 “ dom 𝐻 ) ⊆ dom 𝐹
8 7 a1i ⊢ ( 𝜑 → ( ◡ 𝐹 “ dom 𝐻 ) ⊆ dom 𝐹 )
9 eqid ⊢ dom 𝐹 = dom 𝐹
10 1 2 9 smfdmss ⊢ ( 𝜑 → dom 𝐹 ⊆ ∪ 𝑆 )
11 8 10 sstrd ⊢ ( 𝜑 → ( ◡ 𝐹 “ dom 𝐻 ) ⊆ ∪ 𝑆 )
12 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
13 3 12 eqeltri ⊢ 𝐽 ∈ Top
14 13 a1i ⊢ ( 𝜑 → 𝐽 ∈ Top )
15 14 4 salgencld ⊢ ( 𝜑 → 𝐵 ∈ SAlg )
16 eqid ⊢ dom 𝐻 = dom 𝐻
17 15 5 16 smff ⊢ ( 𝜑 → 𝐻 : dom 𝐻 ⟶ ℝ )
18 17 ffund ⊢ ( 𝜑 → Fun 𝐻 )
19 1 2 9 smff ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
20 19 ffund ⊢ ( 𝜑 → Fun 𝐹 )
21 18 20 funcofd ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) : ( ◡ 𝐹 “ dom 𝐻 ) ⟶ ran 𝐻 )
22 17 frnd ⊢ ( 𝜑 → ran 𝐻 ⊆ ℝ )
23 21 22 fssd ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) : ( ◡ 𝐹 “ dom 𝐻 ) ⟶ ℝ )
24 cnvco ⊢ ◡ ( 𝐻 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ ◡ 𝐻 )
25 24 imaeq1i ⊢ ( ◡ ( 𝐻 ∘ 𝐹 ) “ ( -∞ (,) 𝑎 ) ) = ( ( ◡ 𝐹 ∘ ◡ 𝐻 ) “ ( -∞ (,) 𝑎 ) )
26 23 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝐻 ∘ 𝐹 ) : ( ◡ 𝐹 “ dom 𝐻 ) ⟶ ℝ )
27 rexr ⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℝ* )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ* )
29 26 28 preimaioomnf ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ ( 𝐻 ∘ 𝐹 ) “ ( -∞ (,) 𝑎 ) ) = { 𝑥 ∈ ( ◡ 𝐹 “ dom 𝐻 ) ∣ ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑥 ) < 𝑎 } )
30 imaco ⊢ ( ( ◡ 𝐹 ∘ ◡ 𝐻 ) “ ( -∞ (,) 𝑎 ) ) = ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) )
31 30 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ( ◡ 𝐹 ∘ ◡ 𝐻 ) “ ( -∞ (,) 𝑎 ) ) = ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) )
32 25 29 31 3eqtr3a ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ( ◡ 𝐹 “ dom 𝐻 ) ∣ ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑥 ) < 𝑎 } = ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) )
33 17 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐻 : dom 𝐻 ⟶ ℝ )
34 33 28 preimaioomnf ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = { 𝑥 ∈ dom 𝐻 ∣ ( 𝐻 ‘ 𝑥 ) < 𝑎 } )
35 15 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐵 ∈ SAlg )
36 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐻 ∈ ( SMblFn ‘ 𝐵 ) )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
38 35 36 16 37 smfpreimalt ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ dom 𝐻 ∣ ( 𝐻 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝐵 ↾t dom 𝐻 ) )
39 34 38 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝐵 ↾t dom 𝐻 ) )
40 15 elexd ⊢ ( 𝜑 → 𝐵 ∈ V )
41 5 dmexd ⊢ ( 𝜑 → dom 𝐻 ∈ V )
42 elrest ⊢ ( ( 𝐵 ∈ V ∧ dom 𝐻 ∈ V ) → ( ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝐵 ↾t dom 𝐻 ) ↔ ∃ 𝑒 ∈ 𝐵 ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) ) )
43 40 41 42 syl2anc ⊢ ( 𝜑 → ( ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝐵 ↾t dom 𝐻 ) ↔ ∃ 𝑒 ∈ 𝐵 ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) ) )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝐵 ↾t dom 𝐻 ) ↔ ∃ 𝑒 ∈ 𝐵 ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) ) )
45 39 44 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ∃ 𝑒 ∈ 𝐵 ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) )
46 imaeq2 ⊢ ( ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) = ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) )
47 46 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ∧ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) = ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) )
48 ovexd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( 𝑆 ↾t dom 𝐹 ) ∈ V )
49 2 elexd ⊢ ( 𝜑 → 𝐹 ∈ V )
50 cnvexg ⊢ ( 𝐹 ∈ V → ◡ 𝐹 ∈ V )
51 imaexg ⊢ ( ◡ 𝐹 ∈ V → ( ◡ 𝐹 “ dom 𝐻 ) ∈ V )
52 49 50 51 3syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ dom 𝐻 ) ∈ V )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ◡ 𝐹 “ dom 𝐻 ) ∈ V )
54 1 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → 𝑆 ∈ SAlg )
55 2 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
56 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → 𝑒 ∈ 𝐵 )
57 eqid ⊢ ( ◡ 𝐹 “ 𝑒 ) = ( ◡ 𝐹 “ 𝑒 )
58 54 55 9 3 4 56 57 smfpimbor1 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t dom 𝐹 ) )
59 eqid ⊢ ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) ) = ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) )
60 48 53 58 59 elrestd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) ) ∈ ( ( 𝑆 ↾t dom 𝐹 ) ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
61 inpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) = ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) ) )
62 20 61 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) = ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) ) )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) = ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) ) )
64 2 dmexd ⊢ ( 𝜑 → dom 𝐹 ∈ V )
65 restabs ⊢ ( ( 𝑆 ∈ SAlg ∧ ( ◡ 𝐹 “ dom 𝐻 ) ⊆ dom 𝐹 ∧ dom 𝐹 ∈ V ) → ( ( 𝑆 ↾t dom 𝐹 ) ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) = ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
66 1 8 64 65 syl3anc ⊢ ( 𝜑 → ( ( 𝑆 ↾t dom 𝐹 ) ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) = ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
67 66 eqcomd ⊢ ( 𝜑 → ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) = ( ( 𝑆 ↾t dom 𝐹 ) ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) = ( ( 𝑆 ↾t dom 𝐹 ) ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
69 60 63 68 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
70 69 3adant3 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ∧ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) ) → ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
71 47 70 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ∧ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
72 71 3exp ⊢ ( 𝜑 → ( 𝑒 ∈ 𝐵 → ( ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) ) ) )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑒 ∈ 𝐵 → ( ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) ) ) )
74 73 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∃ 𝑒 ∈ 𝐵 ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) ) )
75 45 74 mpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
76 32 75 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ( ◡ 𝐹 “ dom 𝐻 ) ∣ ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
77 6 1 11 23 76 issmfd ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ ( SMblFn ‘ 𝑆 ) )