Theorem mbfmco2

Description: The pair building of two measurable functions is measurable. ( cf. cnmpt1t ). (Contributed by Thierry Arnoux, 6-Jun-2017)

	Ref	Expression
Hypotheses	mbfmco.1	⊢ ( 𝜑 → 𝑅 ∈ ∪ ran sigAlgebra )
	mbfmco.2	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
	mbfmco.3	⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
	mbfmco2.4	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 MblFnM 𝑆 ) )
	mbfmco2.5	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑅 MblFnM 𝑇 ) )
	mbfmco2.6	⊢ 𝐻 = ( 𝑥 ∈ ∪ 𝑅 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
Assertion	mbfmco2	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MblFnM ( 𝑆 ×s 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mbfmco.1	⊢ ( 𝜑 → 𝑅 ∈ ∪ ran sigAlgebra )
2		mbfmco.2	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
3		mbfmco.3	⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
4		mbfmco2.4	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 MblFnM 𝑆 ) )
5		mbfmco2.5	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑅 MblFnM 𝑇 ) )
6		mbfmco2.6	⊢ 𝐻 = ( 𝑥 ∈ ∪ 𝑅 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
7	1 2 4	mbfmf	⊢ ( 𝜑 → 𝐹 : ∪ 𝑅 ⟶ ∪ 𝑆 )
8	7	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑅 ) → ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝑆 )
9	1 3 5	mbfmf	⊢ ( 𝜑 → 𝐺 : ∪ 𝑅 ⟶ ∪ 𝑇 )
10	9	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑅 ) → ( 𝐺 ‘ 𝑥 ) ∈ ∪ 𝑇 )
11		opelxpi	⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝑆 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ∪ 𝑇 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( ∪ 𝑆 × ∪ 𝑇 ) )
12	8 10 11	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑅 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( ∪ 𝑆 × ∪ 𝑇 ) )
13		sxuni	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ( 𝑆 ×s 𝑇 ) )
14	2 3 13	syl2anc	⊢ ( 𝜑 → ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ( 𝑆 ×s 𝑇 ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑅 ) → ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ( 𝑆 ×s 𝑇 ) )
16	12 15	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑅 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ∪ ( 𝑆 ×s 𝑇 ) )
17	16 6	fmptd	⊢ ( 𝜑 → 𝐻 : ∪ 𝑅 ⟶ ∪ ( 𝑆 ×s 𝑇 ) )
18		eqid	⊢ ( 𝑎 ∈ 𝑆 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 × 𝑏 ) ) = ( 𝑎 ∈ 𝑆 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 × 𝑏 ) )
19		vex	⊢ 𝑎 ∈ V
20		vex	⊢ 𝑏 ∈ V
21	19 20	xpex	⊢ ( 𝑎 × 𝑏 ) ∈ V
22	18 21	elrnmpo	⊢ ( 𝑐 ∈ ran ( 𝑎 ∈ 𝑆 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 × 𝑏 ) ) ↔ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑇 𝑐 = ( 𝑎 × 𝑏 ) )
23		simp3	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) ∧ 𝑐 = ( 𝑎 × 𝑏 ) ) → 𝑐 = ( 𝑎 × 𝑏 ) )
24	23	imaeq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) ∧ 𝑐 = ( 𝑎 × 𝑏 ) ) → ( ◡ 𝐻 “ 𝑐 ) = ( ◡ 𝐻 “ ( 𝑎 × 𝑏 ) ) )
25		simp1	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) ∧ 𝑐 = ( 𝑎 × 𝑏 ) ) → 𝜑 )
26		simp2l	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) ∧ 𝑐 = ( 𝑎 × 𝑏 ) ) → 𝑎 ∈ 𝑆 )
27		simp2r	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) ∧ 𝑐 = ( 𝑎 × 𝑏 ) ) → 𝑏 ∈ 𝑇 )
28	7 9 6	xppreima2	⊢ ( 𝜑 → ( ◡ 𝐻 “ ( 𝑎 × 𝑏 ) ) = ( ( ◡ 𝐹 “ 𝑎 ) ∩ ( ◡ 𝐺 “ 𝑏 ) ) )
29	28	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) → ( ◡ 𝐻 “ ( 𝑎 × 𝑏 ) ) = ( ( ◡ 𝐹 “ 𝑎 ) ∩ ( ◡ 𝐺 “ 𝑏 ) ) )
30	1	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) → 𝑅 ∈ ∪ ran sigAlgebra )
31	2	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) → 𝑆 ∈ ∪ ran sigAlgebra )
32	4	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) → 𝐹 ∈ ( 𝑅 MblFnM 𝑆 ) )
33		simp2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) → 𝑎 ∈ 𝑆 )
34	30 31 32 33	mbfmcnvima	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) → ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑅 )
35	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) → 𝑇 ∈ ∪ ran sigAlgebra )
36	5	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) → 𝐺 ∈ ( 𝑅 MblFnM 𝑇 ) )
37		simp3	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) → 𝑏 ∈ 𝑇 )
38	30 35 36 37	mbfmcnvima	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) → ( ◡ 𝐺 “ 𝑏 ) ∈ 𝑅 )
39		inelsiga	⊢ ( ( 𝑅 ∈ ∪ ran sigAlgebra ∧ ( ◡ 𝐹 “ 𝑎 ) ∈ 𝑅 ∧ ( ◡ 𝐺 “ 𝑏 ) ∈ 𝑅 ) → ( ( ◡ 𝐹 “ 𝑎 ) ∩ ( ◡ 𝐺 “ 𝑏 ) ) ∈ 𝑅 )
40	30 34 38 39	syl3anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) → ( ( ◡ 𝐹 “ 𝑎 ) ∩ ( ◡ 𝐺 “ 𝑏 ) ) ∈ 𝑅 )
41	29 40	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) → ( ◡ 𝐻 “ ( 𝑎 × 𝑏 ) ) ∈ 𝑅 )
42	25 26 27 41	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) ∧ 𝑐 = ( 𝑎 × 𝑏 ) ) → ( ◡ 𝐻 “ ( 𝑎 × 𝑏 ) ) ∈ 𝑅 )
43	24 42	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) ∧ 𝑐 = ( 𝑎 × 𝑏 ) ) → ( ◡ 𝐻 “ 𝑐 ) ∈ 𝑅 )
44	43	3expia	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑇 ) ) → ( 𝑐 = ( 𝑎 × 𝑏 ) → ( ◡ 𝐻 “ 𝑐 ) ∈ 𝑅 ) )
45	44	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑇 𝑐 = ( 𝑎 × 𝑏 ) → ( ◡ 𝐻 “ 𝑐 ) ∈ 𝑅 ) )
46	45	imp	⊢ ( ( 𝜑 ∧ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑇 𝑐 = ( 𝑎 × 𝑏 ) ) → ( ◡ 𝐻 “ 𝑐 ) ∈ 𝑅 )
47	22 46	sylan2b	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ran ( 𝑎 ∈ 𝑆 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 × 𝑏 ) ) ) → ( ◡ 𝐻 “ 𝑐 ) ∈ 𝑅 )
48	47	ralrimiva	⊢ ( 𝜑 → ∀ 𝑐 ∈ ran ( 𝑎 ∈ 𝑆 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 × 𝑏 ) ) ( ◡ 𝐻 “ 𝑐 ) ∈ 𝑅 )
49		eqid	⊢ ran ( 𝑎 ∈ 𝑆 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 × 𝑏 ) ) = ran ( 𝑎 ∈ 𝑆 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 × 𝑏 ) )
50	49	txbasex	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ran ( 𝑎 ∈ 𝑆 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 × 𝑏 ) ) ∈ V )
51	2 3 50	syl2anc	⊢ ( 𝜑 → ran ( 𝑎 ∈ 𝑆 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 × 𝑏 ) ) ∈ V )
52	49	sxval	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×s 𝑇 ) = ( sigaGen ‘ ran ( 𝑎 ∈ 𝑆 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 × 𝑏 ) ) ) )
53	2 3 52	syl2anc	⊢ ( 𝜑 → ( 𝑆 ×s 𝑇 ) = ( sigaGen ‘ ran ( 𝑎 ∈ 𝑆 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 × 𝑏 ) ) ) )
54	51 1 53	imambfm	⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝑅 MblFnM ( 𝑆 ×s 𝑇 ) ) ↔ ( 𝐻 : ∪ 𝑅 ⟶ ∪ ( 𝑆 ×s 𝑇 ) ∧ ∀ 𝑐 ∈ ran ( 𝑎 ∈ 𝑆 , 𝑏 ∈ 𝑇 ↦ ( 𝑎 × 𝑏 ) ) ( ◡ 𝐻 “ 𝑐 ) ∈ 𝑅 ) ) )
55	17 48 54	mpbir2and	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MblFnM ( 𝑆 ×s 𝑇 ) ) )