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 bitrdi ⊢ 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 eqtrdi ⊢ O ∈ V → 𝒫 O MblFn μ 𝔅 ℝ = ℝ O