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 ( 𝑂 ∈ 𝑉 → ( 𝒫 𝑂 MblFnM 𝔅ℝ ) = ( ℝ ↑m 𝑂 ) )

Proof

Step Hyp Ref Expression
1 pwsiga ⊢ ( 𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ ( sigAlgebra ‘ 𝑂 ) )
2 elrnsiga ⊢ ( 𝒫 𝑂 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝒫 𝑂 ∈ ∪ ran sigAlgebra )
3 1 2 syl ⊢ ( 𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ ∪ ran sigAlgebra )
4 brsigarn ⊢ 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ )
5 elrnsiga ⊢ ( 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ ) → 𝔅ℝ ∈ ∪ ran sigAlgebra )
6 4 5 mp1i ⊢ ( 𝑂 ∈ 𝑉 → 𝔅ℝ ∈ ∪ ran sigAlgebra )
7 3 6 ismbfm ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑓 ∈ ( 𝒫 𝑂 MblFnM 𝔅ℝ ) ↔ ( 𝑓 ∈ ( ∪ 𝔅ℝ ↑m ∪ 𝒫 𝑂 ) ∧ ∀ 𝑥 ∈ 𝔅ℝ ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝑂 ) ) )
8 unibrsiga ⊢ ∪ 𝔅ℝ = ℝ
9 reex ⊢ ℝ ∈ V
10 8 9 eqeltri ⊢ ∪ 𝔅ℝ ∈ V
11 unipw ⊢ ∪ 𝒫 𝑂 = 𝑂
12 elex ⊢ ( 𝑂 ∈ 𝑉 → 𝑂 ∈ V )
13 11 12 eqeltrid ⊢ ( 𝑂 ∈ 𝑉 → ∪ 𝒫 𝑂 ∈ V )
14 elmapg ⊢ ( ( ∪ 𝔅ℝ ∈ V ∧ ∪ 𝒫 𝑂 ∈ V ) → ( 𝑓 ∈ ( ∪ 𝔅ℝ ↑m ∪ 𝒫 𝑂 ) ↔ 𝑓 : ∪ 𝒫 𝑂 ⟶ ∪ 𝔅ℝ ) )
15 10 13 14 sylancr ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑓 ∈ ( ∪ 𝔅ℝ ↑m ∪ 𝒫 𝑂 ) ↔ 𝑓 : ∪ 𝒫 𝑂 ⟶ ∪ 𝔅ℝ ) )
16 11 feq2i ⊢ ( 𝑓 : ∪ 𝒫 𝑂 ⟶ ∪ 𝔅ℝ ↔ 𝑓 : 𝑂 ⟶ ∪ 𝔅ℝ )
17 15 16 bitrdi ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑓 ∈ ( ∪ 𝔅ℝ ↑m ∪ 𝒫 𝑂 ) ↔ 𝑓 : 𝑂 ⟶ ∪ 𝔅ℝ ) )
18 ffn ⊢ ( 𝑓 : 𝑂 ⟶ ∪ 𝔅ℝ → 𝑓 Fn 𝑂 )
19 17 18 biimtrdi ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑓 ∈ ( ∪ 𝔅ℝ ↑m ∪ 𝒫 𝑂 ) → 𝑓 Fn 𝑂 ) )
20 elpreima ⊢ ( 𝑓 Fn 𝑂 → ( 𝑦 ∈ ( ◡ 𝑓 “ 𝑥 ) ↔ ( 𝑦 ∈ 𝑂 ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑥 ) ) )
21 simpl ⊢ ( ( 𝑦 ∈ 𝑂 ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑥 ) → 𝑦 ∈ 𝑂 )
22 20 21 biimtrdi ⊢ ( 𝑓 Fn 𝑂 → ( 𝑦 ∈ ( ◡ 𝑓 “ 𝑥 ) → 𝑦 ∈ 𝑂 ) )
23 22 ssrdv ⊢ ( 𝑓 Fn 𝑂 → ( ◡ 𝑓 “ 𝑥 ) ⊆ 𝑂 )
24 vex ⊢ 𝑓 ∈ V
25 24 cnvex ⊢ ◡ 𝑓 ∈ V
26 imaexg ⊢ ( ◡ 𝑓 ∈ V → ( ◡ 𝑓 “ 𝑥 ) ∈ V )
27 25 26 ax-mp ⊢ ( ◡ 𝑓 “ 𝑥 ) ∈ V
28 27 elpw ⊢ ( ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝑂 ↔ ( ◡ 𝑓 “ 𝑥 ) ⊆ 𝑂 )
29 23 28 sylibr ⊢ ( 𝑓 Fn 𝑂 → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝑂 )
30 29 ralrimivw ⊢ ( 𝑓 Fn 𝑂 → ∀ 𝑥 ∈ 𝔅ℝ ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝑂 )
31 19 30 syl6 ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑓 ∈ ( ∪ 𝔅ℝ ↑m ∪ 𝒫 𝑂 ) → ∀ 𝑥 ∈ 𝔅ℝ ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝑂 ) )
32 31 pm4.71d ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑓 ∈ ( ∪ 𝔅ℝ ↑m ∪ 𝒫 𝑂 ) ↔ ( 𝑓 ∈ ( ∪ 𝔅ℝ ↑m ∪ 𝒫 𝑂 ) ∧ ∀ 𝑥 ∈ 𝔅ℝ ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝑂 ) ) )
33 7 32 bitr4d ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑓 ∈ ( 𝒫 𝑂 MblFnM 𝔅ℝ ) ↔ 𝑓 ∈ ( ∪ 𝔅ℝ ↑m ∪ 𝒫 𝑂 ) ) )
34 33 eqrdv ⊢ ( 𝑂 ∈ 𝑉 → ( 𝒫 𝑂 MblFnM 𝔅ℝ ) = ( ∪ 𝔅ℝ ↑m ∪ 𝒫 𝑂 ) )
35 8 11 oveq12i ⊢ ( ∪ 𝔅ℝ ↑m ∪ 𝒫 𝑂 ) = ( ℝ ↑m 𝑂 )
36 34 35 eqtrdi ⊢ ( 𝑂 ∈ 𝑉 → ( 𝒫 𝑂 MblFnM 𝔅ℝ ) = ( ℝ ↑m 𝑂 ) )