Metamath Proof Explorer

Theorem mbfmcst

Description: A constant function is measurable. Cf. mbfconst . (Contributed by Thierry Arnoux, 26-Jan-2017)

Ref Expression
Hypotheses mbfmcst.1 
|- ( ph -> S e. U. ran sigAlgebra )
mbfmcst.2 
|- ( ph -> T e. U. ran sigAlgebra )
mbfmcst.3 
|- ( ph -> F = ( x e. U. S |-> A ) )
mbfmcst.4 
|- ( ph -> A e. U. T )
Assertion mbfmcst 
|- ( ph -> F e. ( S MblFnM T ) )

Proof

Step Hyp Ref Expression
1 mbfmcst.1 
 |-  ( ph -> S e. U. ran sigAlgebra )
2 mbfmcst.2 
 |-  ( ph -> T e. U. ran sigAlgebra )
3 mbfmcst.3 
 |-  ( ph -> F = ( x e. U. S |-> A ) )
4 mbfmcst.4 
 |-  ( ph -> A e. U. T )
5 4 adantr 
 |-  ( ( ph /\ x e. U. S ) -> A e. U. T )
6 3 5 fmpt3d 
 |-  ( ph -> F : U. S --> U. T )
7 unielsiga 
 |-  ( T e. U. ran sigAlgebra -> U. T e. T )
8 2 7 syl 
 |-  ( ph -> U. T e. T )
9 unielsiga 
 |-  ( S e. U. ran sigAlgebra -> U. S e. S )
10 1 9 syl 
 |-  ( ph -> U. S e. S )
11 8 10 elmapd 
 |-  ( ph -> ( F e. ( U. T ^m U. S ) <-> F : U. S --> U. T ) )
12 6 11 mpbird 
 |-  ( ph -> F e. ( U. T ^m U. S ) )
13 fconstmpt 
 |-  ( U. S X. { A } ) = ( x e. U. S |-> A )
14 13 cnveqi 
 |-  `' ( U. S X. { A } ) = `' ( x e. U. S |-> A )
15 cnvxp 
 |-  `' ( U. S X. { A } ) = ( { A } X. U. S )
16 14 15 eqtr3i 
 |-  `' ( x e. U. S |-> A ) = ( { A } X. U. S )
17 16 imaeq1i 
 |-  ( `' ( x e. U. S |-> A ) " y ) = ( ( { A } X. U. S ) " y )
18 df-ima 
 |-  ( ( { A } X. U. S ) " y ) = ran ( ( { A } X. U. S ) |` y )
19 df-rn 
 |-  ran ( ( { A } X. U. S ) |` y ) = dom `' ( ( { A } X. U. S ) |` y )
20 17 18 19 3eqtri 
 |-  ( `' ( x e. U. S |-> A ) " y ) = dom `' ( ( { A } X. U. S ) |` y )
21 df-res 
 |-  ( ( { A } X. U. S ) |` y ) = ( ( { A } X. U. S ) i^i ( y X. _V ) )
22 inxp 
 |-  ( ( { A } X. U. S ) i^i ( y X. _V ) ) = ( ( { A } i^i y ) X. ( U. S i^i _V ) )
23 inv1 
 |-  ( U. S i^i _V ) = U. S
24 23 xpeq2i 
 |-  ( ( { A } i^i y ) X. ( U. S i^i _V ) ) = ( ( { A } i^i y ) X. U. S )
25 21 22 24 3eqtri 
 |-  ( ( { A } X. U. S ) |` y ) = ( ( { A } i^i y ) X. U. S )
26 25 cnveqi 
 |-  `' ( ( { A } X. U. S ) |` y ) = `' ( ( { A } i^i y ) X. U. S )
27 26 dmeqi 
 |-  dom `' ( ( { A } X. U. S ) |` y ) = dom `' ( ( { A } i^i y ) X. U. S )
28 cnvxp 
 |-  `' ( ( { A } i^i y ) X. U. S ) = ( U. S X. ( { A } i^i y ) )
29 28 dmeqi 
 |-  dom `' ( ( { A } i^i y ) X. U. S ) = dom ( U. S X. ( { A } i^i y ) )
30 20 27 29 3eqtri 
 |-  ( `' ( x e. U. S |-> A ) " y ) = dom ( U. S X. ( { A } i^i y ) )
31 xpeq2 
 |-  ( ( { A } i^i y ) = (/) -> ( U. S X. ( { A } i^i y ) ) = ( U. S X. (/) ) )
32 xp0 
 |-  ( U. S X. (/) ) = (/)
33 31 32 eqtrdi 
 |-  ( ( { A } i^i y ) = (/) -> ( U. S X. ( { A } i^i y ) ) = (/) )
34 33 dmeqd 
 |-  ( ( { A } i^i y ) = (/) -> dom ( U. S X. ( { A } i^i y ) ) = dom (/) )
35 dm0 
 |-  dom (/) = (/)
36 34 35 eqtrdi 
 |-  ( ( { A } i^i y ) = (/) -> dom ( U. S X. ( { A } i^i y ) ) = (/) )
37 36 adantl 
 |-  ( ( ph /\ ( { A } i^i y ) = (/) ) -> dom ( U. S X. ( { A } i^i y ) ) = (/) )
38 0elsiga 
 |-  ( S e. U. ran sigAlgebra -> (/) e. S )
39 1 38 syl 
 |-  ( ph -> (/) e. S )
40 39 adantr 
 |-  ( ( ph /\ ( { A } i^i y ) = (/) ) -> (/) e. S )
41 37 40 eqeltrd 
 |-  ( ( ph /\ ( { A } i^i y ) = (/) ) -> dom ( U. S X. ( { A } i^i y ) ) e. S )
42 30 41 eqeltrid 
 |-  ( ( ph /\ ( { A } i^i y ) = (/) ) -> ( `' ( x e. U. S |-> A ) " y ) e. S )
43 dmxp 
 |-  ( ( { A } i^i y ) =/= (/) -> dom ( U. S X. ( { A } i^i y ) ) = U. S )
44 43 adantl 
 |-  ( ( ph /\ ( { A } i^i y ) =/= (/) ) -> dom ( U. S X. ( { A } i^i y ) ) = U. S )
45 10 adantr 
 |-  ( ( ph /\ ( { A } i^i y ) =/= (/) ) -> U. S e. S )
46 44 45 eqeltrd 
 |-  ( ( ph /\ ( { A } i^i y ) =/= (/) ) -> dom ( U. S X. ( { A } i^i y ) ) e. S )
47 30 46 eqeltrid 
 |-  ( ( ph /\ ( { A } i^i y ) =/= (/) ) -> ( `' ( x e. U. S |-> A ) " y ) e. S )
48 42 47 pm2.61dane 
 |-  ( ph -> ( `' ( x e. U. S |-> A ) " y ) e. S )
49 48 ralrimivw 
 |-  ( ph -> A. y e. T ( `' ( x e. U. S |-> A ) " y ) e. S )
50 3 cnveqd 
 |-  ( ph -> `' F = `' ( x e. U. S |-> A ) )
51 50 imaeq1d 
 |-  ( ph -> ( `' F " y ) = ( `' ( x e. U. S |-> A ) " y ) )
52 51 eleq1d 
 |-  ( ph -> ( ( `' F " y ) e. S <-> ( `' ( x e. U. S |-> A ) " y ) e. S ) )
53 52 ralbidv 
 |-  ( ph -> ( A. y e. T ( `' F " y ) e. S <-> A. y e. T ( `' ( x e. U. S |-> A ) " y ) e. S ) )
54 49 53 mpbird 
 |-  ( ph -> A. y e. T ( `' F " y ) e. S )
55 1 2 ismbfm 
 |-  ( ph -> ( F e. ( S MblFnM T ) <-> ( F e. ( U. T ^m U. S ) /\ A. y e. T ( `' F " y ) e. S ) ) )
56 12 54 55 mpbir2and 
 |-  ( ph -> F e. ( S MblFnM T ) )