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		df-res	$⊢ {(\{A\} \times ⋃ S) ↾}_{y} = (\{A\} \times ⋃ S) \cap (y \times V)$
22		inxp	$⊢ (\{A\} \times ⋃ S) \cap (y \times V) = (\{A\} \cap y) \times (⋃ S \cap V)$
23		inv1	$⊢ ⋃ S \cap V = ⋃ S$
24	23	xpeq2i	$⊢ (\{A\} \cap y) \times (⋃ S \cap V) = (\{A\} \cap y) \times ⋃ S$
25	21 22 24	3eqtri	$⊢ {(\{A\} \times ⋃ S) ↾}_{y} = (\{A\} \cap y) \times ⋃ S$
26	25	cnveqi	$⊢ {({(\{A\} \times ⋃ S) ↾}_{y})}^{-1} = {((\{A\} \cap y) \times ⋃ S)}^{-1}$
27	26	dmeqi	$⊢ dom {({(\{A\} \times ⋃ S) ↾}_{y})}^{-1} = dom {((\{A\} \cap y) \times ⋃ S)}^{-1}$
28		cnvxp	$⊢ {((\{A\} \cap y) \times ⋃ S)}^{-1} = ⋃ S \times (\{A\} \cap y)$
29	28	dmeqi	$⊢ dom {((\{A\} \cap y) \times ⋃ S)}^{-1} = dom (⋃ S \times (\{A\} \cap y))$
30	20 27 29	3eqtri	$⊢ {(x \in ⋃ S ⟼ A)}^{-1} [y] = dom (⋃ S \times (\{A\} \cap y))$
31		xpeq2	$⊢ \{A\} \cap y = \emptyset \to ⋃ S \times (\{A\} \cap y) = ⋃ S \times \emptyset$
32		xp0	$⊢ ⋃ S \times \emptyset = \emptyset$
33	31 32	eqtrdi	$⊢ \{A\} \cap y = \emptyset \to ⋃ S \times (\{A\} \cap y) = \emptyset$
34	33	dmeqd	$⊢ \{A\} \cap y = \emptyset \to dom (⋃ S \times (\{A\} \cap y)) = dom \emptyset$
35		dm0	$⊢ dom \emptyset = \emptyset$
36	34 35	eqtrdi	$⊢ \{A\} \cap y = \emptyset \to dom (⋃ S \times (\{A\} \cap y)) = \emptyset$
37	36	adantl	$⊢ (φ \land \{A\} \cap y = \emptyset) \to dom (⋃ S \times (\{A\} \cap y)) = \emptyset$
38		0elsiga	$⊢ S \in ⋃ ran sigAlgebra \to \emptyset \in S$
39	1 38	syl	$⊢ φ \to \emptyset \in S$
40	39	adantr	$⊢ (φ \land \{A\} \cap y = \emptyset) \to \emptyset \in S$
41	37 40	eqeltrd	$⊢ (φ \land \{A\} \cap y = \emptyset) \to dom (⋃ S \times (\{A\} \cap y)) \in S$
42	30 41	eqeltrid	$⊢ (φ \land \{A\} \cap y = \emptyset) \to {(x \in ⋃ S ⟼ A)}^{-1} [y] \in S$
43		dmxp	$⊢ \{A\} \cap y \neq \emptyset \to dom (⋃ S \times (\{A\} \cap y)) = ⋃ S$
44	43	adantl	$⊢ (φ \land \{A\} \cap y \neq \emptyset) \to dom (⋃ S \times (\{A\} \cap y)) = ⋃ S$
45	10	adantr	$⊢ (φ \land \{A\} \cap y \neq \emptyset) \to ⋃ S \in S$
46	44 45	eqeltrd	$⊢ (φ \land \{A\} \cap y \neq \emptyset) \to dom (⋃ S \times (\{A\} \cap y)) \in S$
47	30 46	eqeltrid	$⊢ (φ \land \{A\} \cap y \neq \emptyset) \to {(x \in ⋃ S ⟼ A)}^{-1} [y] \in S$
48	42 47	pm2.61dane	$⊢ φ \to {(x \in ⋃ S ⟼ A)}^{-1} [y] \in S$
49	48	ralrimivw	$⊢ φ \to \forall y \in T {(x \in ⋃ S ⟼ A)}^{-1} [y] \in S$
50	3	cnveqd	$⊢ φ \to F^{-1} = {(x \in ⋃ S ⟼ A)}^{-1}$
51	50	imaeq1d	$⊢ φ \to F^{-1} [y] = {(x \in ⋃ S ⟼ A)}^{-1} [y]$
52	51	eleq1d	$⊢ φ \to (F^{-1} [y] \in S \leftrightarrow {(x \in ⋃ S ⟼ A)}^{-1} [y] \in S)$
53	52	ralbidv	$⊢ φ \to (\forall y \in T F^{-1} [y] \in S \leftrightarrow \forall y \in T {(x \in ⋃ S ⟼ A)}^{-1} [y] \in S)$
54	49 53	mpbird	$⊢ φ \to \forall y \in T F^{-1} [y] \in S$
55	1 2	ismbfm	$⊢ φ \to (F \in (S {MblFn}_{μ} T) \leftrightarrow (F \in ({⋃ T}^{⋃ S}) \land \forall y \in T F^{-1} [y] \in S))$
56	12 54 55	mpbir2and	$⊢ φ \to F \in (S {MblFn}_{μ} T)$

Metamath Proof Explorer

Theorem mbfmcst

Proof