Metamath Proof Explorer

Theorem mbfmco

Description: The composition of two measurable functions is measurable. See cnmpt11 . (Contributed by Thierry Arnoux, 4-Jun-2017)

Ref Expression
Hypotheses mbfmco.1 ⊢ ( 𝜑 → 𝑅 ∈ ∪ ran sigAlgebra )
mbfmco.2 ⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
mbfmco.3 ⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
mbfmco.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 MblFnM 𝑆 ) )
mbfmco.5 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑆 MblFnM 𝑇 ) )
Assertion mbfmco ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 MblFnM 𝑇 ) )

Proof

Step Hyp Ref Expression
1 mbfmco.1 ⊢ ( 𝜑 → 𝑅 ∈ ∪ ran sigAlgebra )
2 mbfmco.2 ⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
3 mbfmco.3 ⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
4 mbfmco.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 MblFnM 𝑆 ) )
5 mbfmco.5 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑆 MblFnM 𝑇 ) )
6 2 3 5 mbfmf ⊢ ( 𝜑 → 𝐺 : ∪ 𝑆 ⟶ ∪ 𝑇 )
7 1 2 4 mbfmf ⊢ ( 𝜑 → 𝐹 : ∪ 𝑅 ⟶ ∪ 𝑆 )
8 fco ⊢ ( ( 𝐺 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ 𝐹 : ∪ 𝑅 ⟶ ∪ 𝑆 ) → ( 𝐺 ∘ 𝐹 ) : ∪ 𝑅 ⟶ ∪ 𝑇 )
9 6 7 8 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) : ∪ 𝑅 ⟶ ∪ 𝑇 )
10 unielsiga ⊢ ( 𝑇 ∈ ∪ ran sigAlgebra → ∪ 𝑇 ∈ 𝑇 )
11 3 10 syl ⊢ ( 𝜑 → ∪ 𝑇 ∈ 𝑇 )
12 unielsiga ⊢ ( 𝑅 ∈ ∪ ran sigAlgebra → ∪ 𝑅 ∈ 𝑅 )
13 1 12 syl ⊢ ( 𝜑 → ∪ 𝑅 ∈ 𝑅 )
14 11 13 elmapd ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) ∈ ( ∪ 𝑇 ↑m ∪ 𝑅 ) ↔ ( 𝐺 ∘ 𝐹 ) : ∪ 𝑅 ⟶ ∪ 𝑇 ) )
15 9 14 mpbird ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ ( ∪ 𝑇 ↑m ∪ 𝑅 ) )
16 cnvco ⊢ ◡ ( 𝐺 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ ◡ 𝐺 )
17 16 imaeq1i ⊢ ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑎 ) = ( ( ◡ 𝐹 ∘ ◡ 𝐺 ) “ 𝑎 )
18 imaco ⊢ ( ( ◡ 𝐹 ∘ ◡ 𝐺 ) “ 𝑎 ) = ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑎 ) )
19 17 18 eqtri ⊢ ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑎 ) = ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑎 ) )
20 1 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑅 ∈ ∪ ran sigAlgebra )
21 2 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑆 ∈ ∪ ran sigAlgebra )
22 4 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝐹 ∈ ( 𝑅 MblFnM 𝑆 ) )
23 3 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑇 ∈ ∪ ran sigAlgebra )
24 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝐺 ∈ ( 𝑆 MblFnM 𝑇 ) )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ∈ 𝑇 )
26 21 23 24 25 mbfmcnvima ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( ◡ 𝐺 “ 𝑎 ) ∈ 𝑆 )
27 20 21 22 26 mbfmcnvima ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑎 ) ) ∈ 𝑅 )
28 19 27 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑎 ) ∈ 𝑅 )
29 28 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑇 ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑎 ) ∈ 𝑅 )
30 1 3 ismbfm ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 MblFnM 𝑇 ) ↔ ( ( 𝐺 ∘ 𝐹 ) ∈ ( ∪ 𝑇 ↑m ∪ 𝑅 ) ∧ ∀ 𝑎 ∈ 𝑇 ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑎 ) ∈ 𝑅 ) ) )
31 15 29 30 mpbir2and ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 MblFnM 𝑇 ) )