# Metamath Proof Explorer

## Theorem mbfmcst

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

Ref Expression
Hypotheses mbfmcst.1 ${⊢}{\phi }\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
mbfmcst.2 ${⊢}{\phi }\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
mbfmcst.3 ${⊢}{\phi }\to {F}=\left({x}\in \bigcup {S}⟼{A}\right)$
mbfmcst.4 ${⊢}{\phi }\to {A}\in \bigcup {T}$
Assertion mbfmcst ${⊢}{\phi }\to {F}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)$

### Proof

Step Hyp Ref Expression
1 mbfmcst.1 ${⊢}{\phi }\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
2 mbfmcst.2 ${⊢}{\phi }\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
3 mbfmcst.3 ${⊢}{\phi }\to {F}=\left({x}\in \bigcup {S}⟼{A}\right)$
4 mbfmcst.4 ${⊢}{\phi }\to {A}\in \bigcup {T}$
5 4 adantr ${⊢}\left({\phi }\wedge {x}\in \bigcup {S}\right)\to {A}\in \bigcup {T}$
6 3 5 fmpt3d ${⊢}{\phi }\to {F}:\bigcup {S}⟶\bigcup {T}$
7 unielsiga ${⊢}{T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \bigcup {T}\in {T}$
8 2 7 syl ${⊢}{\phi }\to \bigcup {T}\in {T}$
9 unielsiga ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \bigcup {S}\in {S}$
10 1 9 syl ${⊢}{\phi }\to \bigcup {S}\in {S}$
11 8 10 elmapd ${⊢}{\phi }\to \left({F}\in \left({\bigcup {T}}^{\bigcup {S}}\right)↔{F}:\bigcup {S}⟶\bigcup {T}\right)$
12 6 11 mpbird ${⊢}{\phi }\to {F}\in \left({\bigcup {T}}^{\bigcup {S}}\right)$
13 fconstmpt ${⊢}\bigcup {S}×\left\{{A}\right\}=\left({x}\in \bigcup {S}⟼{A}\right)$
14 13 cnveqi ${⊢}{\left(\bigcup {S}×\left\{{A}\right\}\right)}^{-1}={\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}$
15 cnvxp ${⊢}{\left(\bigcup {S}×\left\{{A}\right\}\right)}^{-1}=\left\{{A}\right\}×\bigcup {S}$
16 14 15 eqtr3i ${⊢}{\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}=\left\{{A}\right\}×\bigcup {S}$
17 16 imaeq1i ${⊢}{\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}\left[{y}\right]=\left(\left\{{A}\right\}×\bigcup {S}\right)\left[{y}\right]$
18 df-ima ${⊢}\left(\left\{{A}\right\}×\bigcup {S}\right)\left[{y}\right]=\mathrm{ran}\left({\left(\left\{{A}\right\}×\bigcup {S}\right)↾}_{{y}}\right)$
19 df-rn ${⊢}\mathrm{ran}\left({\left(\left\{{A}\right\}×\bigcup {S}\right)↾}_{{y}}\right)=\mathrm{dom}{\left({\left(\left\{{A}\right\}×\bigcup {S}\right)↾}_{{y}}\right)}^{-1}$
20 17 18 19 3eqtri ${⊢}{\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}\left[{y}\right]=\mathrm{dom}{\left({\left(\left\{{A}\right\}×\bigcup {S}\right)↾}_{{y}}\right)}^{-1}$
21 df-res ${⊢}{\left(\left\{{A}\right\}×\bigcup {S}\right)↾}_{{y}}=\left(\left\{{A}\right\}×\bigcup {S}\right)\cap \left({y}×\mathrm{V}\right)$
22 inxp ${⊢}\left(\left\{{A}\right\}×\bigcup {S}\right)\cap \left({y}×\mathrm{V}\right)=\left(\left\{{A}\right\}\cap {y}\right)×\left(\bigcup {S}\cap \mathrm{V}\right)$
23 inv1 ${⊢}\bigcup {S}\cap \mathrm{V}=\bigcup {S}$
24 23 xpeq2i ${⊢}\left(\left\{{A}\right\}\cap {y}\right)×\left(\bigcup {S}\cap \mathrm{V}\right)=\left(\left\{{A}\right\}\cap {y}\right)×\bigcup {S}$
25 21 22 24 3eqtri ${⊢}{\left(\left\{{A}\right\}×\bigcup {S}\right)↾}_{{y}}=\left(\left\{{A}\right\}\cap {y}\right)×\bigcup {S}$
26 25 cnveqi ${⊢}{\left({\left(\left\{{A}\right\}×\bigcup {S}\right)↾}_{{y}}\right)}^{-1}={\left(\left(\left\{{A}\right\}\cap {y}\right)×\bigcup {S}\right)}^{-1}$
27 26 dmeqi ${⊢}\mathrm{dom}{\left({\left(\left\{{A}\right\}×\bigcup {S}\right)↾}_{{y}}\right)}^{-1}=\mathrm{dom}{\left(\left(\left\{{A}\right\}\cap {y}\right)×\bigcup {S}\right)}^{-1}$
28 cnvxp ${⊢}{\left(\left(\left\{{A}\right\}\cap {y}\right)×\bigcup {S}\right)}^{-1}=\bigcup {S}×\left(\left\{{A}\right\}\cap {y}\right)$
29 28 dmeqi ${⊢}\mathrm{dom}{\left(\left(\left\{{A}\right\}\cap {y}\right)×\bigcup {S}\right)}^{-1}=\mathrm{dom}\left(\bigcup {S}×\left(\left\{{A}\right\}\cap {y}\right)\right)$
30 20 27 29 3eqtri ${⊢}{\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}\left[{y}\right]=\mathrm{dom}\left(\bigcup {S}×\left(\left\{{A}\right\}\cap {y}\right)\right)$
31 xpeq2 ${⊢}\left\{{A}\right\}\cap {y}=\varnothing \to \bigcup {S}×\left(\left\{{A}\right\}\cap {y}\right)=\bigcup {S}×\varnothing$
32 xp0 ${⊢}\bigcup {S}×\varnothing =\varnothing$
33 31 32 syl6eq ${⊢}\left\{{A}\right\}\cap {y}=\varnothing \to \bigcup {S}×\left(\left\{{A}\right\}\cap {y}\right)=\varnothing$
34 33 dmeqd ${⊢}\left\{{A}\right\}\cap {y}=\varnothing \to \mathrm{dom}\left(\bigcup {S}×\left(\left\{{A}\right\}\cap {y}\right)\right)=\mathrm{dom}\varnothing$
35 dm0 ${⊢}\mathrm{dom}\varnothing =\varnothing$
36 34 35 syl6eq ${⊢}\left\{{A}\right\}\cap {y}=\varnothing \to \mathrm{dom}\left(\bigcup {S}×\left(\left\{{A}\right\}\cap {y}\right)\right)=\varnothing$
37 36 adantl ${⊢}\left({\phi }\wedge \left\{{A}\right\}\cap {y}=\varnothing \right)\to \mathrm{dom}\left(\bigcup {S}×\left(\left\{{A}\right\}\cap {y}\right)\right)=\varnothing$
38 0elsiga ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \varnothing \in {S}$
39 1 38 syl ${⊢}{\phi }\to \varnothing \in {S}$
40 39 adantr ${⊢}\left({\phi }\wedge \left\{{A}\right\}\cap {y}=\varnothing \right)\to \varnothing \in {S}$
41 37 40 eqeltrd ${⊢}\left({\phi }\wedge \left\{{A}\right\}\cap {y}=\varnothing \right)\to \mathrm{dom}\left(\bigcup {S}×\left(\left\{{A}\right\}\cap {y}\right)\right)\in {S}$
42 30 41 eqeltrid ${⊢}\left({\phi }\wedge \left\{{A}\right\}\cap {y}=\varnothing \right)\to {\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}\left[{y}\right]\in {S}$
43 dmxp ${⊢}\left\{{A}\right\}\cap {y}\ne \varnothing \to \mathrm{dom}\left(\bigcup {S}×\left(\left\{{A}\right\}\cap {y}\right)\right)=\bigcup {S}$
44 43 adantl ${⊢}\left({\phi }\wedge \left\{{A}\right\}\cap {y}\ne \varnothing \right)\to \mathrm{dom}\left(\bigcup {S}×\left(\left\{{A}\right\}\cap {y}\right)\right)=\bigcup {S}$
45 10 adantr ${⊢}\left({\phi }\wedge \left\{{A}\right\}\cap {y}\ne \varnothing \right)\to \bigcup {S}\in {S}$
46 44 45 eqeltrd ${⊢}\left({\phi }\wedge \left\{{A}\right\}\cap {y}\ne \varnothing \right)\to \mathrm{dom}\left(\bigcup {S}×\left(\left\{{A}\right\}\cap {y}\right)\right)\in {S}$
47 30 46 eqeltrid ${⊢}\left({\phi }\wedge \left\{{A}\right\}\cap {y}\ne \varnothing \right)\to {\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}\left[{y}\right]\in {S}$
48 42 47 pm2.61dane ${⊢}{\phi }\to {\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}\left[{y}\right]\in {S}$
49 48 ralrimivw ${⊢}{\phi }\to \forall {y}\in {T}\phantom{\rule{.4em}{0ex}}{\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}\left[{y}\right]\in {S}$
50 3 cnveqd ${⊢}{\phi }\to {{F}}^{-1}={\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}$
51 50 imaeq1d ${⊢}{\phi }\to {{F}}^{-1}\left[{y}\right]={\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}\left[{y}\right]$
52 51 eleq1d ${⊢}{\phi }\to \left({{F}}^{-1}\left[{y}\right]\in {S}↔{\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}\left[{y}\right]\in {S}\right)$
53 52 ralbidv ${⊢}{\phi }\to \left(\forall {y}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{y}\right]\in {S}↔\forall {y}\in {T}\phantom{\rule{.4em}{0ex}}{\left({x}\in \bigcup {S}⟼{A}\right)}^{-1}\left[{y}\right]\in {S}\right)$
54 49 53 mpbird ${⊢}{\phi }\to \forall {y}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{y}\right]\in {S}$
55 1 2 ismbfm ${⊢}{\phi }\to \left({F}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)↔\left({F}\in \left({\bigcup {T}}^{\bigcup {S}}\right)\wedge \forall {y}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{y}\right]\in {S}\right)\right)$
56 12 54 55 mpbir2and ${⊢}{\phi }\to {F}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)$