Metamath Proof Explorer

Theorem ismbfm

Description: The predicate " F is a measurable function from the measurable space S to the measurable space T ". Cf. ismbf . (Contributed by Thierry Arnoux, 23-Jan-2017)

Ref Expression
Hypotheses ismbfm.1 ( 𝜑𝑆 ran sigAlgebra )
ismbfm.2 ( 𝜑𝑇 ran sigAlgebra )
Assertion ismbfm ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ ( 𝐹 ∈ ( 𝑇m 𝑆 ) ∧ ∀ 𝑥𝑇 ( 𝐹𝑥 ) ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 ismbfm.1 ( 𝜑𝑆 ran sigAlgebra )
2 ismbfm.2 ( 𝜑𝑇 ran sigAlgebra )
3 unieq ( 𝑠 = 𝑆 𝑠 = 𝑆 )
4 3 oveq2d ( 𝑠 = 𝑆 → ( 𝑡m 𝑠 ) = ( 𝑡m 𝑆 ) )
5 eleq2 ( 𝑠 = 𝑆 → ( ( 𝑓𝑥 ) ∈ 𝑠 ↔ ( 𝑓𝑥 ) ∈ 𝑆 ) )
6 5 ralbidv ( 𝑠 = 𝑆 → ( ∀ 𝑥𝑡 ( 𝑓𝑥 ) ∈ 𝑠 ↔ ∀ 𝑥𝑡 ( 𝑓𝑥 ) ∈ 𝑆 ) )
7 4 6 rabeqbidv ( 𝑠 = 𝑆 → { 𝑓 ∈ ( 𝑡m 𝑠 ) ∣ ∀ 𝑥𝑡 ( 𝑓𝑥 ) ∈ 𝑠 } = { 𝑓 ∈ ( 𝑡m 𝑆 ) ∣ ∀ 𝑥𝑡 ( 𝑓𝑥 ) ∈ 𝑆 } )
8 unieq ( 𝑡 = 𝑇 𝑡 = 𝑇 )
9 8 oveq1d ( 𝑡 = 𝑇 → ( 𝑡m 𝑆 ) = ( 𝑇m 𝑆 ) )
10 raleq ( 𝑡 = 𝑇 → ( ∀ 𝑥𝑡 ( 𝑓𝑥 ) ∈ 𝑆 ↔ ∀ 𝑥𝑇 ( 𝑓𝑥 ) ∈ 𝑆 ) )
11 9 10 rabeqbidv ( 𝑡 = 𝑇 → { 𝑓 ∈ ( 𝑡m 𝑆 ) ∣ ∀ 𝑥𝑡 ( 𝑓𝑥 ) ∈ 𝑆 } = { 𝑓 ∈ ( 𝑇m 𝑆 ) ∣ ∀ 𝑥𝑇 ( 𝑓𝑥 ) ∈ 𝑆 } )
12 df-mbfm MblFnM = ( 𝑠 ran sigAlgebra , 𝑡 ran sigAlgebra ↦ { 𝑓 ∈ ( 𝑡m 𝑠 ) ∣ ∀ 𝑥𝑡 ( 𝑓𝑥 ) ∈ 𝑠 } )
13 ovex ( 𝑇m 𝑆 ) ∈ V
14 13 rabex { 𝑓 ∈ ( 𝑇m 𝑆 ) ∣ ∀ 𝑥𝑇 ( 𝑓𝑥 ) ∈ 𝑆 } ∈ V
15 7 11 12 14 ovmpo ( ( 𝑆 ran sigAlgebra ∧ 𝑇 ran sigAlgebra ) → ( 𝑆 MblFnM 𝑇 ) = { 𝑓 ∈ ( 𝑇m 𝑆 ) ∣ ∀ 𝑥𝑇 ( 𝑓𝑥 ) ∈ 𝑆 } )
16 1 2 15 syl2anc ( 𝜑 → ( 𝑆 MblFnM 𝑇 ) = { 𝑓 ∈ ( 𝑇m 𝑆 ) ∣ ∀ 𝑥𝑇 ( 𝑓𝑥 ) ∈ 𝑆 } )
17 16 eleq2d ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝑇m 𝑆 ) ∣ ∀ 𝑥𝑇 ( 𝑓𝑥 ) ∈ 𝑆 } ) )
18 cnveq ( 𝑓 = 𝐹 𝑓 = 𝐹 )
19 18 imaeq1d ( 𝑓 = 𝐹 → ( 𝑓𝑥 ) = ( 𝐹𝑥 ) )
20 19 eleq1d ( 𝑓 = 𝐹 → ( ( 𝑓𝑥 ) ∈ 𝑆 ↔ ( 𝐹𝑥 ) ∈ 𝑆 ) )
21 20 ralbidv ( 𝑓 = 𝐹 → ( ∀ 𝑥𝑇 ( 𝑓𝑥 ) ∈ 𝑆 ↔ ∀ 𝑥𝑇 ( 𝐹𝑥 ) ∈ 𝑆 ) )
22 21 elrab ( 𝐹 ∈ { 𝑓 ∈ ( 𝑇m 𝑆 ) ∣ ∀ 𝑥𝑇 ( 𝑓𝑥 ) ∈ 𝑆 } ↔ ( 𝐹 ∈ ( 𝑇m 𝑆 ) ∧ ∀ 𝑥𝑇 ( 𝐹𝑥 ) ∈ 𝑆 ) )
23 17 22 syl6bb ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ ( 𝐹 ∈ ( 𝑇m 𝑆 ) ∧ ∀ 𝑥𝑇 ( 𝐹𝑥 ) ∈ 𝑆 ) ) )