# Metamath Proof Explorer

## Theorem mbfmcnt

Description: All functions are measurable with respect to the counting measure. (Contributed by Thierry Arnoux, 24-Jan-2017)

Ref Expression
Assertion mbfmcnt ${⊢}{O}\in {V}\to 𝒫{O}{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}={ℝ}^{{O}}$

### Proof

Step Hyp Ref Expression
1 pwsiga ${⊢}{O}\in {V}\to 𝒫{O}\in \mathrm{sigAlgebra}\left({O}\right)$
2 elrnsiga ${⊢}𝒫{O}\in \mathrm{sigAlgebra}\left({O}\right)\to 𝒫{O}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
3 1 2 syl ${⊢}{O}\in {V}\to 𝒫{O}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
4 brsigarn ${⊢}{𝔅}_{ℝ}\in \mathrm{sigAlgebra}\left(ℝ\right)$
5 elrnsiga ${⊢}{𝔅}_{ℝ}\in \mathrm{sigAlgebra}\left(ℝ\right)\to {𝔅}_{ℝ}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
6 4 5 mp1i ${⊢}{O}\in {V}\to {𝔅}_{ℝ}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
7 3 6 ismbfm ${⊢}{O}\in {V}\to \left({f}\in \left(𝒫{O}{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)↔\left({f}\in \left({\bigcup {𝔅}_{ℝ}}^{\bigcup 𝒫{O}}\right)\wedge \forall {x}\in {𝔅}_{ℝ}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in 𝒫{O}\right)\right)$
8 unibrsiga ${⊢}\bigcup {𝔅}_{ℝ}=ℝ$
9 reex ${⊢}ℝ\in \mathrm{V}$
10 8 9 eqeltri ${⊢}\bigcup {𝔅}_{ℝ}\in \mathrm{V}$
11 unipw ${⊢}\bigcup 𝒫{O}={O}$
12 elex ${⊢}{O}\in {V}\to {O}\in \mathrm{V}$
13 11 12 eqeltrid ${⊢}{O}\in {V}\to \bigcup 𝒫{O}\in \mathrm{V}$
14 elmapg ${⊢}\left(\bigcup {𝔅}_{ℝ}\in \mathrm{V}\wedge \bigcup 𝒫{O}\in \mathrm{V}\right)\to \left({f}\in \left({\bigcup {𝔅}_{ℝ}}^{\bigcup 𝒫{O}}\right)↔{f}:\bigcup 𝒫{O}⟶\bigcup {𝔅}_{ℝ}\right)$
15 10 13 14 sylancr ${⊢}{O}\in {V}\to \left({f}\in \left({\bigcup {𝔅}_{ℝ}}^{\bigcup 𝒫{O}}\right)↔{f}:\bigcup 𝒫{O}⟶\bigcup {𝔅}_{ℝ}\right)$
16 11 feq2i ${⊢}{f}:\bigcup 𝒫{O}⟶\bigcup {𝔅}_{ℝ}↔{f}:{O}⟶\bigcup {𝔅}_{ℝ}$
17 15 16 syl6bb ${⊢}{O}\in {V}\to \left({f}\in \left({\bigcup {𝔅}_{ℝ}}^{\bigcup 𝒫{O}}\right)↔{f}:{O}⟶\bigcup {𝔅}_{ℝ}\right)$
18 ffn ${⊢}{f}:{O}⟶\bigcup {𝔅}_{ℝ}\to {f}Fn{O}$
19 17 18 syl6bi ${⊢}{O}\in {V}\to \left({f}\in \left({\bigcup {𝔅}_{ℝ}}^{\bigcup 𝒫{O}}\right)\to {f}Fn{O}\right)$
20 elpreima ${⊢}{f}Fn{O}\to \left({y}\in {{f}}^{-1}\left[{x}\right]↔\left({y}\in {O}\wedge {f}\left({y}\right)\in {x}\right)\right)$
21 simpl ${⊢}\left({y}\in {O}\wedge {f}\left({y}\right)\in {x}\right)\to {y}\in {O}$
22 20 21 syl6bi ${⊢}{f}Fn{O}\to \left({y}\in {{f}}^{-1}\left[{x}\right]\to {y}\in {O}\right)$
23 22 ssrdv ${⊢}{f}Fn{O}\to {{f}}^{-1}\left[{x}\right]\subseteq {O}$
24 vex ${⊢}{f}\in \mathrm{V}$
25 24 cnvex ${⊢}{{f}}^{-1}\in \mathrm{V}$
26 imaexg ${⊢}{{f}}^{-1}\in \mathrm{V}\to {{f}}^{-1}\left[{x}\right]\in \mathrm{V}$
27 25 26 ax-mp ${⊢}{{f}}^{-1}\left[{x}\right]\in \mathrm{V}$
28 27 elpw ${⊢}{{f}}^{-1}\left[{x}\right]\in 𝒫{O}↔{{f}}^{-1}\left[{x}\right]\subseteq {O}$
29 23 28 sylibr ${⊢}{f}Fn{O}\to {{f}}^{-1}\left[{x}\right]\in 𝒫{O}$
30 29 ralrimivw ${⊢}{f}Fn{O}\to \forall {x}\in {𝔅}_{ℝ}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in 𝒫{O}$
31 19 30 syl6 ${⊢}{O}\in {V}\to \left({f}\in \left({\bigcup {𝔅}_{ℝ}}^{\bigcup 𝒫{O}}\right)\to \forall {x}\in {𝔅}_{ℝ}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in 𝒫{O}\right)$
32 31 pm4.71d ${⊢}{O}\in {V}\to \left({f}\in \left({\bigcup {𝔅}_{ℝ}}^{\bigcup 𝒫{O}}\right)↔\left({f}\in \left({\bigcup {𝔅}_{ℝ}}^{\bigcup 𝒫{O}}\right)\wedge \forall {x}\in {𝔅}_{ℝ}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{x}\right]\in 𝒫{O}\right)\right)$
33 7 32 bitr4d ${⊢}{O}\in {V}\to \left({f}\in \left(𝒫{O}{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)↔{f}\in \left({\bigcup {𝔅}_{ℝ}}^{\bigcup 𝒫{O}}\right)\right)$
34 33 eqrdv ${⊢}{O}\in {V}\to 𝒫{O}{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}={\bigcup {𝔅}_{ℝ}}^{\bigcup 𝒫{O}}$
35 8 11 oveq12i ${⊢}{\bigcup {𝔅}_{ℝ}}^{\bigcup 𝒫{O}}={ℝ}^{{O}}$
36 34 35 syl6eq ${⊢}{O}\in {V}\to 𝒫{O}{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}={ℝ}^{{O}}$