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 V 𝒫 O MblFn μ 𝔅 = O

Proof

Step Hyp Ref Expression
1 pwsiga O V 𝒫 O sigAlgebra O
2 elrnsiga 𝒫 O sigAlgebra O 𝒫 O ran sigAlgebra
3 1 2 syl O V 𝒫 O ran sigAlgebra
4 brsigarn 𝔅 sigAlgebra
5 elrnsiga 𝔅 sigAlgebra 𝔅 ran sigAlgebra
6 4 5 mp1i O V 𝔅 ran sigAlgebra
7 3 6 ismbfm O V f 𝒫 O MblFn μ 𝔅 f 𝔅 𝒫 O x 𝔅 f -1 x 𝒫 O
8 unibrsiga 𝔅 =
9 reex V
10 8 9 eqeltri 𝔅 V
11 unipw 𝒫 O = O
12 elex O V O V
13 11 12 eqeltrid O V 𝒫 O V
14 elmapg 𝔅 V 𝒫 O V f 𝔅 𝒫 O f : 𝒫 O 𝔅
15 10 13 14 sylancr O V f 𝔅 𝒫 O f : 𝒫 O 𝔅
16 11 feq2i f : 𝒫 O 𝔅 f : O 𝔅
17 15 16 syl6bb O V f 𝔅 𝒫 O f : O 𝔅
18 ffn f : O 𝔅 f Fn O
19 17 18 syl6bi O V f 𝔅 𝒫 O f Fn O
20 elpreima f Fn O y f -1 x y O f y x
21 simpl y O f y x y O
22 20 21 syl6bi f Fn O y f -1 x y O
23 22 ssrdv f Fn O f -1 x O
24 vex f V
25 24 cnvex f -1 V
26 imaexg f -1 V f -1 x V
27 25 26 ax-mp f -1 x V
28 27 elpw f -1 x 𝒫 O f -1 x O
29 23 28 sylibr f Fn O f -1 x 𝒫 O
30 29 ralrimivw f Fn O x 𝔅 f -1 x 𝒫 O
31 19 30 syl6 O V f 𝔅 𝒫 O x 𝔅 f -1 x 𝒫 O
32 31 pm4.71d O V f 𝔅 𝒫 O f 𝔅 𝒫 O x 𝔅 f -1 x 𝒫 O
33 7 32 bitr4d O V f 𝒫 O MblFn μ 𝔅 f 𝔅 𝒫 O
34 33 eqrdv O V 𝒫 O MblFn μ 𝔅 = 𝔅 𝒫 O
35 8 11 oveq12i 𝔅 𝒫 O = O
36 34 35 syl6eq O V 𝒫 O MblFn μ 𝔅 = O