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→𝒫OMblFnμ𝔅ℝ=ℝ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∈𝒫OMblFnμ𝔅ℝ↔f∈⋃𝔅ℝ⋃𝒫O∧∀x∈𝔅ℝf-1x∈𝒫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 bitrdi ⊢O∈V→f∈⋃𝔅ℝ⋃𝒫O↔f:O⟶⋃𝔅ℝ
18 ffn ⊢f:O⟶⋃𝔅ℝ→fFnO
19 17 18 syl6bi ⊢O∈V→f∈⋃𝔅ℝ⋃𝒫O→fFnO
20 elpreima ⊢fFnO→y∈f-1x↔y∈O∧f⁡y∈x
21 simpl ⊢y∈O∧f⁡y∈x→y∈O
22 20 21 syl6bi ⊢fFnO→y∈f-1x→y∈O
23 22 ssrdv ⊢fFnO→f-1x⊆O
24 vex ⊢f∈V
25 24 cnvex ⊢f-1∈V
26 imaexg ⊢f-1∈V→f-1x∈V
27 25 26 ax-mp ⊢f-1x∈V
28 27 elpw ⊢f-1x∈𝒫O↔f-1x⊆O
29 23 28 sylibr ⊢fFnO→f-1x∈𝒫O
30 29 ralrimivw ⊢fFnO→∀x∈𝔅ℝf-1x∈𝒫O
31 19 30 syl6 ⊢O∈V→f∈⋃𝔅ℝ⋃𝒫O→∀x∈𝔅ℝf-1x∈𝒫O
32 31 pm4.71d ⊢O∈V→f∈⋃𝔅ℝ⋃𝒫O↔f∈⋃𝔅ℝ⋃𝒫O∧∀x∈𝔅ℝf-1x∈𝒫O
33 7 32 bitr4d ⊢O∈V→f∈𝒫OMblFnμ𝔅ℝ↔f∈⋃𝔅ℝ⋃𝒫O
34 33 eqrdv ⊢O∈V→𝒫OMblFnμ𝔅ℝ=⋃𝔅ℝ⋃𝒫O
35 8 11 oveq12i ⊢⋃𝔅ℝ⋃𝒫O=ℝO
36 34 35 eqtrdi ⊢O∈V→𝒫OMblFnμ𝔅ℝ=ℝO