Metamath Proof Explorer


Theorem elunirnmbfm

Description: The property of being a measurable function. (Contributed by Thierry Arnoux, 23-Jan-2017)

Ref Expression
Assertion elunirnmbfm F ran MblFn μ s ran sigAlgebra t ran sigAlgebra F t s x t F -1 x s

Proof

Step Hyp Ref Expression
1 df-mbfm MblFn μ = s ran sigAlgebra , t ran sigAlgebra f t s | x t f -1 x s
2 1 mpofun Fun MblFn μ
3 elunirn Fun MblFn μ F ran MblFn μ a dom MblFn μ F MblFn μ a
4 2 3 ax-mp F ran MblFn μ a dom MblFn μ F MblFn μ a
5 ovex t s V
6 5 rabex f t s | x t f -1 x s V
7 1 6 dmmpo dom MblFn μ = ran sigAlgebra × ran sigAlgebra
8 7 rexeqi a dom MblFn μ F MblFn μ a a ran sigAlgebra × ran sigAlgebra F MblFn μ a
9 fveq2 a = s t MblFn μ a = MblFn μ s t
10 df-ov s MblFn μ t = MblFn μ s t
11 9 10 syl6eqr a = s t MblFn μ a = s MblFn μ t
12 11 eleq2d a = s t F MblFn μ a F s MblFn μ t
13 12 rexxp a ran sigAlgebra × ran sigAlgebra F MblFn μ a s ran sigAlgebra t ran sigAlgebra F s MblFn μ t
14 4 8 13 3bitri F ran MblFn μ s ran sigAlgebra t ran sigAlgebra F s MblFn μ t
15 simpl s ran sigAlgebra t ran sigAlgebra s ran sigAlgebra
16 simpr s ran sigAlgebra t ran sigAlgebra t ran sigAlgebra
17 15 16 ismbfm s ran sigAlgebra t ran sigAlgebra F s MblFn μ t F t s x t F -1 x s
18 17 2rexbiia s ran sigAlgebra t ran sigAlgebra F s MblFn μ t s ran sigAlgebra t ran sigAlgebra F t s x t F -1 x s
19 14 18 bitri F ran MblFn μ s ran sigAlgebra t ran sigAlgebra F t s x t F -1 x s