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 syl6bb ( 𝑂𝑉 → ( 𝑓 ∈ ( 𝔅m 𝒫 𝑂 ) ↔ 𝑓 : 𝑂 𝔅 ) )
18 ffn ( 𝑓 : 𝑂 𝔅𝑓 Fn 𝑂 )
19 17 18 syl6bi ( 𝑂𝑉 → ( 𝑓 ∈ ( 𝔅m 𝒫 𝑂 ) → 𝑓 Fn 𝑂 ) )
20 elpreima ( 𝑓 Fn 𝑂 → ( 𝑦 ∈ ( 𝑓𝑥 ) ↔ ( 𝑦𝑂 ∧ ( 𝑓𝑦 ) ∈ 𝑥 ) ) )
21 simpl ( ( 𝑦𝑂 ∧ ( 𝑓𝑦 ) ∈ 𝑥 ) → 𝑦𝑂 )
22 20 21 syl6bi ( 𝑓 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 𝑂 ) )