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 fco3 ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) : ( ◡ 𝐹 “ dom 𝐻 ) ⟶ ran 𝐻 )
22 17 frnd ⊢ ( 𝜑 → ran 𝐻 ⊆ ℝ )
23 21 22 fssd ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) : ( ◡ 𝐹 “ dom 𝐻 ) ⟶ ℝ )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝐻 ∘ 𝐹 ) : ( ◡ 𝐹 “ dom 𝐻 ) ⟶ ℝ )
25 rexr ⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℝ* )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ* )
27 24 26 preimaioomnf ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ ( 𝐻 ∘ 𝐹 ) “ ( -∞ (,) 𝑎 ) ) = { 𝑥 ∈ ( ◡ 𝐹 “ dom 𝐻 ) ∣ ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑥 ) < 𝑎 } )
28 27 eqcomd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ( ◡ 𝐹 “ dom 𝐻 ) ∣ ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑥 ) < 𝑎 } = ( ◡ ( 𝐻 ∘ 𝐹 ) “ ( -∞ (,) 𝑎 ) ) )
29 cnvco ⊢ ◡ ( 𝐻 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ ◡ 𝐻 )
30 29 imaeq1i ⊢ ( ◡ ( 𝐻 ∘ 𝐹 ) “ ( -∞ (,) 𝑎 ) ) = ( ( ◡ 𝐹 ∘ ◡ 𝐻 ) “ ( -∞ (,) 𝑎 ) )
31 30 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ ( 𝐻 ∘ 𝐹 ) “ ( -∞ (,) 𝑎 ) ) = ( ( ◡ 𝐹 ∘ ◡ 𝐻 ) “ ( -∞ (,) 𝑎 ) ) )
32 imaco ⊢ ( ( ◡ 𝐹 ∘ ◡ 𝐻 ) “ ( -∞ (,) 𝑎 ) ) = ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) )
33 32 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ( ◡ 𝐹 ∘ ◡ 𝐻 ) “ ( -∞ (,) 𝑎 ) ) = ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) )
34 28 31 33 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ( ◡ 𝐹 “ dom 𝐻 ) ∣ ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑥 ) < 𝑎 } = ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) )
35 17 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐻 : dom 𝐻 ⟶ ℝ )
36 35 26 preimaioomnf ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = { 𝑥 ∈ dom 𝐻 ∣ ( 𝐻 ‘ 𝑥 ) < 𝑎 } )
37 36 eqcomd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ dom 𝐻 ∣ ( 𝐻 ‘ 𝑥 ) < 𝑎 } = ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) )
38 37 eqcomd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = { 𝑥 ∈ dom 𝐻 ∣ ( 𝐻 ‘ 𝑥 ) < 𝑎 } )
39 15 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐵 ∈ SAlg )
40 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐻 ∈ ( SMblFn ‘ 𝐵 ) )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
42 39 40 16 41 smfpreimalt ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ dom 𝐻 ∣ ( 𝐻 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝐵 ↾t dom 𝐻 ) )
43 38 42 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝐵 ↾t dom 𝐻 ) )
44 15 elexd ⊢ ( 𝜑 → 𝐵 ∈ V )
45 5 dmexd ⊢ ( 𝜑 → dom 𝐻 ∈ V )
46 elrest ⊢ ( ( 𝐵 ∈ V ∧ dom 𝐻 ∈ V ) → ( ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝐵 ↾t dom 𝐻 ) ↔ ∃ 𝑒 ∈ 𝐵 ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) ) )
47 44 45 46 syl2anc ⊢ ( 𝜑 → ( ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝐵 ↾t dom 𝐻 ) ↔ ∃ 𝑒 ∈ 𝐵 ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝐵 ↾t dom 𝐻 ) ↔ ∃ 𝑒 ∈ 𝐵 ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) ) )
49 43 48 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ∃ 𝑒 ∈ 𝐵 ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) )
50 imaeq2 ⊢ ( ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) = ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) )
51 50 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ∧ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) = ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) )
52 ovexd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( 𝑆 ↾t dom 𝐹 ) ∈ V )
53 2 elexd ⊢ ( 𝜑 → 𝐹 ∈ V )
54 cnvexg ⊢ ( 𝐹 ∈ V → ◡ 𝐹 ∈ V )
55 53 54 syl ⊢ ( 𝜑 → ◡ 𝐹 ∈ V )
56 imaexg ⊢ ( ◡ 𝐹 ∈ V → ( ◡ 𝐹 “ dom 𝐻 ) ∈ V )
57 55 56 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ dom 𝐻 ) ∈ V )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ◡ 𝐹 “ dom 𝐻 ) ∈ V )
59 1 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → 𝑆 ∈ SAlg )
60 2 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
61 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → 𝑒 ∈ 𝐵 )
62 eqid ⊢ ( ◡ 𝐹 “ 𝑒 ) = ( ◡ 𝐹 “ 𝑒 )
63 59 60 9 3 4 61 62 smfpimbor1 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t dom 𝐹 ) )
64 eqid ⊢ ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) ) = ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) )
65 52 58 63 64 elrestd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) ) ∈ ( ( 𝑆 ↾t dom 𝐹 ) ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
66 inpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) = ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) ) )
67 20 66 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) = ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) ) )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) = ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) ) )
69 2 dmexd ⊢ ( 𝜑 → dom 𝐹 ∈ V )
70 restabs ⊢ ( ( 𝑆 ∈ SAlg ∧ ( ◡ 𝐹 “ dom 𝐻 ) ⊆ dom 𝐹 ∧ dom 𝐹 ∈ V ) → ( ( 𝑆 ↾t dom 𝐹 ) ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) = ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
71 1 8 69 70 syl3anc ⊢ ( 𝜑 → ( ( 𝑆 ↾t dom 𝐹 ) ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) = ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
72 71 eqcomd ⊢ ( 𝜑 → ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) = ( ( 𝑆 ↾t dom 𝐹 ) ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) = ( ( 𝑆 ↾t dom 𝐹 ) ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
74 68 73 eleq12d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) ↔ ( ( ◡ 𝐹 “ 𝑒 ) ∩ ( ◡ 𝐹 “ dom 𝐻 ) ) ∈ ( ( 𝑆 ↾t dom 𝐹 ) ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) ) )
75 65 74 mpbird ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
76 75 3adant3 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ∧ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) ) → ( ◡ 𝐹 “ ( 𝑒 ∩ dom 𝐻 ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
77 51 76 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ∧ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
78 77 3exp ⊢ ( 𝜑 → ( 𝑒 ∈ 𝐵 → ( ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) ) ) )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑒 ∈ 𝐵 → ( ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) ) ) )
80 79 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∃ 𝑒 ∈ 𝐵 ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) = ( 𝑒 ∩ dom 𝐻 ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) ) )
81 49 80 mpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐹 “ ( ◡ 𝐻 “ ( -∞ (,) 𝑎 ) ) ) ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
82 34 81 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ( ◡ 𝐹 “ dom 𝐻 ) ∣ ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t ( ◡ 𝐹 “ dom 𝐻 ) ) )
83 6 1 11 23 82 issmfd ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ ( SMblFn ‘ 𝑆 ) )