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 e. V -> ( ~P O MblFnM BrSiga ) = ( RR ^m O ) )

Proof

Step	Hyp	Ref	Expression
1		pwsiga	|- ( O e. V -> ~P O e. ( sigAlgebra ` O ) )
2		elrnsiga	|- ( ~P O e. ( sigAlgebra ` O ) -> ~P O e. U. ran sigAlgebra )
3	1 2	syl	|- ( O e. V -> ~P O e. U. ran sigAlgebra )
4		brsigarn	|- BrSiga e. ( sigAlgebra ` RR )
5		elrnsiga	|- ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga e. U. ran sigAlgebra )
6	4 5	mp1i	|- ( O e. V -> BrSiga e. U. ran sigAlgebra )
7	3 6	ismbfm	|- ( O e. V -> ( f e. ( ~P O MblFnM BrSiga ) <-> ( f e. ( U. BrSiga ^m U. ~P O ) /\ A. x e. BrSiga ( `' f " x ) e. ~P O ) ) )
8		unibrsiga	|- U. BrSiga = RR
9		reex	|- RR e. _V
10	8 9	eqeltri	|- U. BrSiga e. _V
11		unipw	|- U. ~P O = O
12		elex	|- ( O e. V -> O e. _V )
13	11 12	eqeltrid	|- ( O e. V -> U. ~P O e. _V )
14		elmapg	|- ( ( U. BrSiga e. _V /\ U. ~P O e. _V ) -> ( f e. ( U. BrSiga ^m U. ~P O ) <-> f : U. ~P O --> U. BrSiga ) )
15	10 13 14	sylancr	|- ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) <-> f : U. ~P O --> U. BrSiga ) )
16	11	feq2i	|- ( f : U. ~P O --> U. BrSiga <-> f : O --> U. BrSiga )
17	15 16	bitrdi	|- ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) <-> f : O --> U. BrSiga ) )
18		ffn	|- ( f : O --> U. BrSiga -> f Fn O )
19	17 18	syl6bi	|- ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) -> f Fn O ) )
20		elpreima	|- ( f Fn O -> ( y e. ( `' f " x ) <-> ( y e. O /\ ( f ` y ) e. x ) ) )
21		simpl	|- ( ( y e. O /\ ( f ` y ) e. x ) -> y e. O )
22	20 21	syl6bi	|- ( f Fn O -> ( y e. ( `' f " x ) -> y e. O ) )
23	22	ssrdv	|- ( f Fn O -> ( `' f " x ) C_ O )
24		vex	|- f e. _V
25	24	cnvex	|- `' f e. _V
26		imaexg	|- ( `' f e. _V -> ( `' f " x ) e. _V )
27	25 26	ax-mp	|- ( `' f " x ) e. _V
28	27	elpw	|- ( ( `' f " x ) e. ~P O <-> ( `' f " x ) C_ O )
29	23 28	sylibr	|- ( f Fn O -> ( `' f " x ) e. ~P O )
30	29	ralrimivw	|- ( f Fn O -> A. x e. BrSiga ( `' f " x ) e. ~P O )
31	19 30	syl6	|- ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) -> A. x e. BrSiga ( `' f " x ) e. ~P O ) )
32	31	pm4.71d	|- ( O e. V -> ( f e. ( U. BrSiga ^m U. ~P O ) <-> ( f e. ( U. BrSiga ^m U. ~P O ) /\ A. x e. BrSiga ( `' f " x ) e. ~P O ) ) )
33	7 32	bitr4d	|- ( O e. V -> ( f e. ( ~P O MblFnM BrSiga ) <-> f e. ( U. BrSiga ^m U. ~P O ) ) )
34	33	eqrdv	|- ( O e. V -> ( ~P O MblFnM BrSiga ) = ( U. BrSiga ^m U. ~P O ) )
35	8 11	oveq12i	|- ( U. BrSiga ^m U. ~P O ) = ( RR ^m O )
36	34 35	eqtrdi	|- ( O e. V -> ( ~P O MblFnM BrSiga ) = ( RR ^m O ) )