mbfmcst

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

	Ref	Expression
Hypotheses	mbfmcst.1	$⊢ φ \to S \in ⋃ ran sigAlgebra$
	mbfmcst.2	$⊢ φ \to T \in ⋃ ran sigAlgebra$
	mbfmcst.3	$⊢ φ \to F = (x \in ⋃ S ⟼ A)$
	mbfmcst.4	$⊢ φ \to A \in ⋃ T$
Assertion	mbfmcst	$⊢ φ \to F \in (S {MblFn}_{μ} T)$

Proof

Step	Hyp	Ref	Expression
1		mbfmcst.1	$⊢ φ \to S \in ⋃ ran sigAlgebra$
2		mbfmcst.2	$⊢ φ \to T \in ⋃ ran sigAlgebra$
3		mbfmcst.3	$⊢ φ \to F = (x \in ⋃ S ⟼ A)$
4		mbfmcst.4	$⊢ φ \to A \in ⋃ T$
5	4	adantr	$⊢ (φ \land x \in ⋃ S) \to A \in ⋃ T$
6	3 5	fmpt3d	$⊢ φ \to F : ⋃ S ⟶ ⋃ T$
7		unielsiga	$⊢ T \in ⋃ ran sigAlgebra \to ⋃ T \in T$
8	2 7	syl	$⊢ φ \to ⋃ T \in T$
9		unielsiga	$⊢ S \in ⋃ ran sigAlgebra \to ⋃ S \in S$
10	1 9	syl	$⊢ φ \to ⋃ S \in S$
11	8 10	elmapd	$⊢ φ \to (F \in ({⋃ T}^{⋃ S}) \leftrightarrow F : ⋃ S ⟶ ⋃ T)$
12	6 11	mpbird	$⊢ φ \to F \in ({⋃ T}^{⋃ S})$
13		fconstmpt	$⊢ ⋃ S \times \{A\} = (x \in ⋃ S ⟼ A)$
14	13	cnveqi	$⊢ {(⋃ S \times \{A\})}^{-1} = {(x \in ⋃ S ⟼ A)}^{-1}$
15		cnvxp	$⊢ {(⋃ S \times \{A\})}^{-1} = \{A\} \times ⋃ S$
16	14 15	eqtr3i	$⊢ {(x \in ⋃ S ⟼ A)}^{-1} = \{A\} \times ⋃ S$
17	16	imaeq1i	$⊢ {(x \in ⋃ S ⟼ A)}^{-1} [y] = (\{A\} \times ⋃ S) [y]$
18		df-ima	$⊢ (\{A\} \times ⋃ S) [y] = ran ({(\{A\} \times ⋃ S) ↾}_{y})$
19		df-rn	$⊢ ran ({(\{A\} \times ⋃ S) ↾}_{y}) = dom {({(\{A\} \times ⋃ S) ↾}_{y})}^{-1}$
20	17 18 19	3eqtri	$⊢ {(x \in ⋃ S ⟼ A)}^{-1} [y] = dom {({(\{A\} \times ⋃ S) ↾}_{y})}^{-1}$
21		xpres	$⊢ {(\{A\} \times ⋃ S) ↾}_{y} = (\{A\} \cap y) \times ⋃ S$
22	21	cnveqi	$⊢ {({(\{A\} \times ⋃ S) ↾}_{y})}^{-1} = {((\{A\} \cap y) \times ⋃ S)}^{-1}$
23	22	dmeqi	$⊢ dom {({(\{A\} \times ⋃ S) ↾}_{y})}^{-1} = dom {((\{A\} \cap y) \times ⋃ S)}^{-1}$
24		cnvxp	$⊢ {((\{A\} \cap y) \times ⋃ S)}^{-1} = ⋃ S \times (\{A\} \cap y)$
25	24	dmeqi	$⊢ dom {((\{A\} \cap y) \times ⋃ S)}^{-1} = dom (⋃ S \times (\{A\} \cap y))$
26	20 23 25	3eqtri	$⊢ {(x \in ⋃ S ⟼ A)}^{-1} [y] = dom (⋃ S \times (\{A\} \cap y))$
27		xpeq2	$⊢ \{A\} \cap y = \emptyset \to ⋃ S \times (\{A\} \cap y) = ⋃ S \times \emptyset$
28		xp0	$⊢ ⋃ S \times \emptyset = \emptyset$
29	27 28	eqtrdi	$⊢ \{A\} \cap y = \emptyset \to ⋃ S \times (\{A\} \cap y) = \emptyset$
30	29	dmeqd	$⊢ \{A\} \cap y = \emptyset \to dom (⋃ S \times (\{A\} \cap y)) = dom \emptyset$
31		dm0	$⊢ dom \emptyset = \emptyset$
32	30 31	eqtrdi	$⊢ \{A\} \cap y = \emptyset \to dom (⋃ S \times (\{A\} \cap y)) = \emptyset$
33	32	adantl	$⊢ (φ \land \{A\} \cap y = \emptyset) \to dom (⋃ S \times (\{A\} \cap y)) = \emptyset$
34		0elsiga	$⊢ S \in ⋃ ran sigAlgebra \to \emptyset \in S$
35	1 34	syl	$⊢ φ \to \emptyset \in S$
36	35	adantr	$⊢ (φ \land \{A\} \cap y = \emptyset) \to \emptyset \in S$
37	33 36	eqeltrd	$⊢ (φ \land \{A\} \cap y = \emptyset) \to dom (⋃ S \times (\{A\} \cap y)) \in S$
38	26 37	eqeltrid	$⊢ (φ \land \{A\} \cap y = \emptyset) \to {(x \in ⋃ S ⟼ A)}^{-1} [y] \in S$
39		dmxp	$⊢ \{A\} \cap y \neq \emptyset \to dom (⋃ S \times (\{A\} \cap y)) = ⋃ S$
40	39	adantl	$⊢ (φ \land \{A\} \cap y \neq \emptyset) \to dom (⋃ S \times (\{A\} \cap y)) = ⋃ S$
41	10	adantr	$⊢ (φ \land \{A\} \cap y \neq \emptyset) \to ⋃ S \in S$
42	40 41	eqeltrd	$⊢ (φ \land \{A\} \cap y \neq \emptyset) \to dom (⋃ S \times (\{A\} \cap y)) \in S$
43	26 42	eqeltrid	$⊢ (φ \land \{A\} \cap y \neq \emptyset) \to {(x \in ⋃ S ⟼ A)}^{-1} [y] \in S$
44	38 43	pm2.61dane	$⊢ φ \to {(x \in ⋃ S ⟼ A)}^{-1} [y] \in S$
45	44	ralrimivw	$⊢ φ \to \forall y \in T {(x \in ⋃ S ⟼ A)}^{-1} [y] \in S$
46	3	cnveqd	$⊢ φ \to F^{-1} = {(x \in ⋃ S ⟼ A)}^{-1}$
47	46	imaeq1d	$⊢ φ \to F^{-1} [y] = {(x \in ⋃ S ⟼ A)}^{-1} [y]$
48	47	eleq1d	$⊢ φ \to (F^{-1} [y] \in S \leftrightarrow {(x \in ⋃ S ⟼ A)}^{-1} [y] \in S)$
49	48	ralbidv	$⊢ φ \to (\forall y \in T F^{-1} [y] \in S \leftrightarrow \forall y \in T {(x \in ⋃ S ⟼ A)}^{-1} [y] \in S)$
50	45 49	mpbird	$⊢ φ \to \forall y \in T F^{-1} [y] \in S$
51	1 2	ismbfm	$⊢ φ \to (F \in (S {MblFn}_{μ} T) \leftrightarrow (F \in ({⋃ T}^{⋃ S}) \land \forall y \in T F^{-1} [y] \in S))$
52	12 50 51	mpbir2and	$⊢ φ \to F \in (S {MblFn}_{μ} T)$

Metamath Proof Explorer

Theorem mbfmcst

Proof