Theorem mbfmcst

Description: A constant function is measurable. Cf. mbfconst . (Contributed by Thierry Arnoux, 26-Jan-2017)

	Ref	Expression
Hypotheses	mbfmcst.1	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
	mbfmcst.2	⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
	mbfmcst.3	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) )
	mbfmcst.4	⊢ ( 𝜑 → 𝐴 ∈ ∪ 𝑇 )
Assertion	mbfmcst	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		mbfmcst.1	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
2		mbfmcst.2	⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
3		mbfmcst.3	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) )
4		mbfmcst.4	⊢ ( 𝜑 → 𝐴 ∈ ∪ 𝑇 )
5	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑆 ) → 𝐴 ∈ ∪ 𝑇 )
6	3 5	fmpt3d	⊢ ( 𝜑 → 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 )
7		unielsiga	⊢ ( 𝑇 ∈ ∪ ran sigAlgebra → ∪ 𝑇 ∈ 𝑇 )
8	2 7	syl	⊢ ( 𝜑 → ∪ 𝑇 ∈ 𝑇 )
9		unielsiga	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆 )
10	1 9	syl	⊢ ( 𝜑 → ∪ 𝑆 ∈ 𝑆 )
11	8 10	elmapd	⊢ ( 𝜑 → ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ↔ 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 ) )
12	6 11	mpbird	⊢ ( 𝜑 → 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) )
13		fconstmpt	⊢ ( ∪ 𝑆 × { 𝐴 } ) = ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 )
14	13	cnveqi	⊢ ◡ ( ∪ 𝑆 × { 𝐴 } ) = ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 )
15		cnvxp	⊢ ◡ ( ∪ 𝑆 × { 𝐴 } ) = ( { 𝐴 } × ∪ 𝑆 )
16	14 15	eqtr3i	⊢ ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) = ( { 𝐴 } × ∪ 𝑆 )
17	16	imaeq1i	⊢ ( ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) “ 𝑦 ) = ( ( { 𝐴 } × ∪ 𝑆 ) “ 𝑦 )
18		df-ima	⊢ ( ( { 𝐴 } × ∪ 𝑆 ) “ 𝑦 ) = ran ( ( { 𝐴 } × ∪ 𝑆 ) ↾ 𝑦 )
19		df-rn	⊢ ran ( ( { 𝐴 } × ∪ 𝑆 ) ↾ 𝑦 ) = dom ◡ ( ( { 𝐴 } × ∪ 𝑆 ) ↾ 𝑦 )
20	17 18 19	3eqtri	⊢ ( ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) “ 𝑦 ) = dom ◡ ( ( { 𝐴 } × ∪ 𝑆 ) ↾ 𝑦 )
21		df-res	⊢ ( ( { 𝐴 } × ∪ 𝑆 ) ↾ 𝑦 ) = ( ( { 𝐴 } × ∪ 𝑆 ) ∩ ( 𝑦 × V ) )
22		inxp	⊢ ( ( { 𝐴 } × ∪ 𝑆 ) ∩ ( 𝑦 × V ) ) = ( ( { 𝐴 } ∩ 𝑦 ) × ( ∪ 𝑆 ∩ V ) )
23		inv1	⊢ ( ∪ 𝑆 ∩ V ) = ∪ 𝑆
24	23	xpeq2i	⊢ ( ( { 𝐴 } ∩ 𝑦 ) × ( ∪ 𝑆 ∩ V ) ) = ( ( { 𝐴 } ∩ 𝑦 ) × ∪ 𝑆 )
25	21 22 24	3eqtri	⊢ ( ( { 𝐴 } × ∪ 𝑆 ) ↾ 𝑦 ) = ( ( { 𝐴 } ∩ 𝑦 ) × ∪ 𝑆 )
26	25	cnveqi	⊢ ◡ ( ( { 𝐴 } × ∪ 𝑆 ) ↾ 𝑦 ) = ◡ ( ( { 𝐴 } ∩ 𝑦 ) × ∪ 𝑆 )
27	26	dmeqi	⊢ dom ◡ ( ( { 𝐴 } × ∪ 𝑆 ) ↾ 𝑦 ) = dom ◡ ( ( { 𝐴 } ∩ 𝑦 ) × ∪ 𝑆 )
28		cnvxp	⊢ ◡ ( ( { 𝐴 } ∩ 𝑦 ) × ∪ 𝑆 ) = ( ∪ 𝑆 × ( { 𝐴 } ∩ 𝑦 ) )
29	28	dmeqi	⊢ dom ◡ ( ( { 𝐴 } ∩ 𝑦 ) × ∪ 𝑆 ) = dom ( ∪ 𝑆 × ( { 𝐴 } ∩ 𝑦 ) )
30	20 27 29	3eqtri	⊢ ( ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) “ 𝑦 ) = dom ( ∪ 𝑆 × ( { 𝐴 } ∩ 𝑦 ) )
31		xpeq2	⊢ ( ( { 𝐴 } ∩ 𝑦 ) = ∅ → ( ∪ 𝑆 × ( { 𝐴 } ∩ 𝑦 ) ) = ( ∪ 𝑆 × ∅ ) )
32		xp0	⊢ ( ∪ 𝑆 × ∅ ) = ∅
33	31 32	eqtrdi	⊢ ( ( { 𝐴 } ∩ 𝑦 ) = ∅ → ( ∪ 𝑆 × ( { 𝐴 } ∩ 𝑦 ) ) = ∅ )
34	33	dmeqd	⊢ ( ( { 𝐴 } ∩ 𝑦 ) = ∅ → dom ( ∪ 𝑆 × ( { 𝐴 } ∩ 𝑦 ) ) = dom ∅ )
35		dm0	⊢ dom ∅ = ∅
36	34 35	eqtrdi	⊢ ( ( { 𝐴 } ∩ 𝑦 ) = ∅ → dom ( ∪ 𝑆 × ( { 𝐴 } ∩ 𝑦 ) ) = ∅ )
37	36	adantl	⊢ ( ( 𝜑 ∧ ( { 𝐴 } ∩ 𝑦 ) = ∅ ) → dom ( ∪ 𝑆 × ( { 𝐴 } ∩ 𝑦 ) ) = ∅ )
38		0elsiga	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆 )
39	1 38	syl	⊢ ( 𝜑 → ∅ ∈ 𝑆 )
40	39	adantr	⊢ ( ( 𝜑 ∧ ( { 𝐴 } ∩ 𝑦 ) = ∅ ) → ∅ ∈ 𝑆 )
41	37 40	eqeltrd	⊢ ( ( 𝜑 ∧ ( { 𝐴 } ∩ 𝑦 ) = ∅ ) → dom ( ∪ 𝑆 × ( { 𝐴 } ∩ 𝑦 ) ) ∈ 𝑆 )
42	30 41	eqeltrid	⊢ ( ( 𝜑 ∧ ( { 𝐴 } ∩ 𝑦 ) = ∅ ) → ( ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) “ 𝑦 ) ∈ 𝑆 )
43		dmxp	⊢ ( ( { 𝐴 } ∩ 𝑦 ) ≠ ∅ → dom ( ∪ 𝑆 × ( { 𝐴 } ∩ 𝑦 ) ) = ∪ 𝑆 )
44	43	adantl	⊢ ( ( 𝜑 ∧ ( { 𝐴 } ∩ 𝑦 ) ≠ ∅ ) → dom ( ∪ 𝑆 × ( { 𝐴 } ∩ 𝑦 ) ) = ∪ 𝑆 )
45	10	adantr	⊢ ( ( 𝜑 ∧ ( { 𝐴 } ∩ 𝑦 ) ≠ ∅ ) → ∪ 𝑆 ∈ 𝑆 )
46	44 45	eqeltrd	⊢ ( ( 𝜑 ∧ ( { 𝐴 } ∩ 𝑦 ) ≠ ∅ ) → dom ( ∪ 𝑆 × ( { 𝐴 } ∩ 𝑦 ) ) ∈ 𝑆 )
47	30 46	eqeltrid	⊢ ( ( 𝜑 ∧ ( { 𝐴 } ∩ 𝑦 ) ≠ ∅ ) → ( ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) “ 𝑦 ) ∈ 𝑆 )
48	42 47	pm2.61dane	⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) “ 𝑦 ) ∈ 𝑆 )
49	48	ralrimivw	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑇 ( ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) “ 𝑦 ) ∈ 𝑆 )
50	3	cnveqd	⊢ ( 𝜑 → ◡ 𝐹 = ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) )
51	50	imaeq1d	⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑦 ) = ( ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) “ 𝑦 ) )
52	51	eleq1d	⊢ ( 𝜑 → ( ( ◡ 𝐹 “ 𝑦 ) ∈ 𝑆 ↔ ( ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) “ 𝑦 ) ∈ 𝑆 ) )
53	52	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑇 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝑆 ↔ ∀ 𝑦 ∈ 𝑇 ( ◡ ( 𝑥 ∈ ∪ 𝑆 ↦ 𝐴 ) “ 𝑦 ) ∈ 𝑆 ) )
54	49 53	mpbird	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑇 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝑆 )
55	1 2	ismbfm	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∧ ∀ 𝑦 ∈ 𝑇 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝑆 ) ) )
56	12 54 55	mpbir2and	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )