Metamath Proof Explorer

Theorem smfconst

Description: Given a sigma-algebra over a base set X, every partial real-valued constant function is measurable. Proposition 121E (a) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfconst.x 
|- F/ x ph
smfconst.s 
|- ( ph -> S e. SAlg )
smfconst.a 
|- ( ph -> A C_ U. S )
smfconst.b 
|- ( ph -> B e. RR )
smfconst.f 
|- F = ( x e. A |-> B )
Assertion smfconst 
|- ( ph -> F e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfconst.x 
 |-  F/ x ph
2 smfconst.s 
 |-  ( ph -> S e. SAlg )
3 smfconst.a 
 |-  ( ph -> A C_ U. S )
4 smfconst.b 
 |-  ( ph -> B e. RR )
5 smfconst.f 
 |-  F = ( x e. A |-> B )
6 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
7 5 6 nfcxfr 
 |-  F/_ x F
8 nfv 
 |-  F/ a ph
9 4 adantr 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
10 1 9 5 fmptdf 
 |-  ( ph -> F : A --> RR )
11 nfv 
 |-  F/ x a e. RR
12 1 11 nfan 
 |-  F/ x ( ph /\ a e. RR )
13 nfv 
 |-  F/ x B < a
14 12 13 nfan 
 |-  F/ x ( ( ph /\ a e. RR ) /\ B < a )
15 4 ad2antrr 
 |-  ( ( ( ph /\ a e. RR ) /\ B < a ) -> B e. RR )
16 simpr 
 |-  ( ( ( ph /\ a e. RR ) /\ B < a ) -> B < a )
17 14 15 5 16 pimconstlt1 
 |-  ( ( ( ph /\ a e. RR ) /\ B < a ) -> { x e. A | ( F ` x ) < a } = A )
18 eqidd 
 |-  ( ( ( ph /\ a e. RR ) /\ B < a ) -> A = A )
19 sseqin2 
 |-  ( A C_ U. S <-> ( U. S i^i A ) = A )
20 3 19 sylib 
 |-  ( ph -> ( U. S i^i A ) = A )
21 20 eqcomd 
 |-  ( ph -> A = ( U. S i^i A ) )
22 21 ad2antrr 
 |-  ( ( ( ph /\ a e. RR ) /\ B < a ) -> A = ( U. S i^i A ) )
23 17 18 22 3eqtrd 
 |-  ( ( ( ph /\ a e. RR ) /\ B < a ) -> { x e. A | ( F ` x ) < a } = ( U. S i^i A ) )
24 2 ad2antrr 
 |-  ( ( ( ph /\ a e. RR ) /\ B < a ) -> S e. SAlg )
25 2 uniexd 
 |-  ( ph -> U. S e. _V )
26 25 3 ssexd 
 |-  ( ph -> A e. _V )
27 26 ad2antrr 
 |-  ( ( ( ph /\ a e. RR ) /\ B < a ) -> A e. _V )
28 24 salunid 
 |-  ( ( ( ph /\ a e. RR ) /\ B < a ) -> U. S e. S )
29 eqid 
 |-  ( U. S i^i A ) = ( U. S i^i A )
30 24 27 28 29 elrestd 
 |-  ( ( ( ph /\ a e. RR ) /\ B < a ) -> ( U. S i^i A ) e. ( S |`t A ) )
31 23 30 eqeltrd 
 |-  ( ( ( ph /\ a e. RR ) /\ B < a ) -> { x e. A | ( F ` x ) < a } e. ( S |`t A ) )
32 nfv 
 |-  F/ x -. B < a
33 12 32 nfan 
 |-  F/ x ( ( ph /\ a e. RR ) /\ -. B < a )
34 4 ad2antrr 
 |-  ( ( ( ph /\ a e. RR ) /\ -. B < a ) -> B e. RR )
35 rexr 
 |-  ( a e. RR -> a e. RR* )
36 35 ad2antlr 
 |-  ( ( ( ph /\ a e. RR ) /\ -. B < a ) -> a e. RR* )
37 simpr 
 |-  ( ( ( ph /\ a e. RR ) /\ -. B < a ) -> -. B < a )
38 simplr 
 |-  ( ( ( ph /\ a e. RR ) /\ -. B < a ) -> a e. RR )
39 38 34 lenltd 
 |-  ( ( ( ph /\ a e. RR ) /\ -. B < a ) -> ( a <_ B <-> -. B < a ) )
40 37 39 mpbird 
 |-  ( ( ( ph /\ a e. RR ) /\ -. B < a ) -> a <_ B )
41 33 34 5 36 40 pimconstlt0 
 |-  ( ( ( ph /\ a e. RR ) /\ -. B < a ) -> { x e. A | ( F ` x ) < a } = (/) )
42 eqid 
 |-  ( S |`t A ) = ( S |`t A )
43 2 26 42 subsalsal 
 |-  ( ph -> ( S |`t A ) e. SAlg )
44 43 0sald 
 |-  ( ph -> (/) e. ( S |`t A ) )
45 44 ad2antrr 
 |-  ( ( ( ph /\ a e. RR ) /\ -. B < a ) -> (/) e. ( S |`t A ) )
46 41 45 eqeltrd 
 |-  ( ( ( ph /\ a e. RR ) /\ -. B < a ) -> { x e. A | ( F ` x ) < a } e. ( S |`t A ) )
47 31 46 pm2.61dan 
 |-  ( ( ph /\ a e. RR ) -> { x e. A | ( F ` x ) < a } e. ( S |`t A ) )
48 7 8 2 3 10 47 issmfdf 
 |-  ( ph -> F e. ( SMblFn ` S ) )