cnmbfm

Description: A continuous function is measurable with respect to the Borel Algebra of its domain and range. (Contributed by Thierry Arnoux, 3-Jun-2017)

	Ref	Expression
Hypotheses	cnmbfm.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
	cnmbfm.2	⊢ ( 𝜑 → 𝑆 = ( sigaGen ‘ 𝐽 ) )
	cnmbfm.3	⊢ ( 𝜑 → 𝑇 = ( sigaGen ‘ 𝐾 ) )
Assertion	cnmbfm	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		cnmbfm.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
2		cnmbfm.2	⊢ ( 𝜑 → 𝑆 = ( sigaGen ‘ 𝐽 ) )
3		cnmbfm.3	⊢ ( 𝜑 → 𝑇 = ( sigaGen ‘ 𝐾 ) )
4		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
5		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
6	4 5	cnf	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
7	1 6	syl	⊢ ( 𝜑 → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
8	2	unieqd	⊢ ( 𝜑 → ∪ 𝑆 = ∪ ( sigaGen ‘ 𝐽 ) )
9		cntop1	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
10		unisg	⊢ ( 𝐽 ∈ Top → ∪ ( sigaGen ‘ 𝐽 ) = ∪ 𝐽 )
11	1 9 10	3syl	⊢ ( 𝜑 → ∪ ( sigaGen ‘ 𝐽 ) = ∪ 𝐽 )
12	8 11	eqtrd	⊢ ( 𝜑 → ∪ 𝑆 = ∪ 𝐽 )
13	3	unieqd	⊢ ( 𝜑 → ∪ 𝑇 = ∪ ( sigaGen ‘ 𝐾 ) )
14		cntop2	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
15		unisg	⊢ ( 𝐾 ∈ Top → ∪ ( sigaGen ‘ 𝐾 ) = ∪ 𝐾 )
16	1 14 15	3syl	⊢ ( 𝜑 → ∪ ( sigaGen ‘ 𝐾 ) = ∪ 𝐾 )
17	13 16	eqtrd	⊢ ( 𝜑 → ∪ 𝑇 = ∪ 𝐾 )
18	12 17	feq23d	⊢ ( 𝜑 → ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ↔ 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ) )
19	7 18	mpbird	⊢ ( 𝜑 → 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 )
20		sssigagen	⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ ( sigaGen ‘ 𝐽 ) )
21	1 9 20	3syl	⊢ ( 𝜑 → 𝐽 ⊆ ( sigaGen ‘ 𝐽 ) )
22	21 2	sseqtrrd	⊢ ( 𝜑 → 𝐽 ⊆ 𝑆 )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → 𝐽 ⊆ 𝑆 )
24		cnima	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑎 ∈ 𝐾 ) → ( ^◡ 𝐹 “ 𝑎 ) ∈ 𝐽 )
25	1 24	sylan	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → ( ^◡ 𝐹 “ 𝑎 ) ∈ 𝐽 )
26	23 25	sseldd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐾 ) → ( ^◡ 𝐹 “ 𝑎 ) ∈ 𝑆 )
27	26	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐾 ( ^◡ 𝐹 “ 𝑎 ) ∈ 𝑆 )
28		elex	⊢ ( 𝐾 ∈ Top → 𝐾 ∈ V )
29	1 14 28	3syl	⊢ ( 𝜑 → 𝐾 ∈ V )
30		sigagensiga	⊢ ( 𝐽 ∈ Top → ( sigaGen ‘ 𝐽 ) ∈ ( sigAlgebra ‘ ∪ 𝐽 ) )
31	1 9 30	3syl	⊢ ( 𝜑 → ( sigaGen ‘ 𝐽 ) ∈ ( sigAlgebra ‘ ∪ 𝐽 ) )
32	2 31	eqeltrd	⊢ ( 𝜑 → 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝐽 ) )
33		elrnsiga	⊢ ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝐽 ) → 𝑆 ∈ ∪ ran sigAlgebra )
34	32 33	syl	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
35	29 34 3	imambfm	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ ( 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ∧ ∀ 𝑎 ∈ 𝐾 ( ^◡ 𝐹 “ 𝑎 ) ∈ 𝑆 ) ) )
36	19 27 35	mpbir2and	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )

Metamath Proof Explorer

Theorem cnmbfm

Proof