Metamath Proof Explorer


Theorem issmfgt

Description: The predicate " F is a real-valued measurable function w.r.t. to the sigma-algebra S ". A function is measurable iff the preimages of all left-open intervals unbounded above are in the subspace sigma-algebra induced by its domain. The domain of F is required to be b subset of the underlying set of S . Definition 121C of Fremlin1 p. 36, and Proposition 121B (iii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmfgt.s φSSAlg
issmfgt.d D=domF
Assertion issmfgt φFSMblFnSDSF:DaxD|a<FxS𝑡D

Proof

Step Hyp Ref Expression
1 issmfgt.s φSSAlg
2 issmfgt.d D=domF
3 1 adantr φFSMblFnSSSAlg
4 simpr φFSMblFnSFSMblFnS
5 3 4 2 smfdmss φFSMblFnSDS
6 3 4 2 smff φFSMblFnSF:D
7 nfv bφ
8 nfv bFSMblFnS
9 7 8 nfan bφFSMblFnS
10 3 5 restuni4 φFSMblFnSS𝑡D=D
11 10 eqcomd φFSMblFnSD=S𝑡D
12 11 rabeqdv φFSMblFnSyD|b<Fy=yS𝑡D|b<Fy
13 12 adantr φFSMblFnSbyD|b<Fy=yS𝑡D|b<Fy
14 nfv yφ
15 nfv yFSMblFnS
16 14 15 nfan yφFSMblFnS
17 nfv yb
18 16 17 nfan yφFSMblFnSb
19 nfv cφFSMblFnSb
20 1 uniexd φSV
21 20 adantr φDSSV
22 simpr φDSDS
23 21 22 ssexd φDSDV
24 5 23 syldan φFSMblFnSDV
25 eqid S𝑡D=S𝑡D
26 3 24 25 subsalsal φFSMblFnSS𝑡DSAlg
27 26 adantr φFSMblFnSbS𝑡DSAlg
28 eqid S𝑡D=S𝑡D
29 6 adantr φFSMblFnSyS𝑡DF:D
30 simpr φFSMblFnSyS𝑡DyS𝑡D
31 10 adantr φFSMblFnSyS𝑡DS𝑡D=D
32 30 31 eleqtrd φFSMblFnSyS𝑡DyD
33 29 32 ffvelrnd φFSMblFnSyS𝑡DFy
34 33 rexrd φFSMblFnSyS𝑡DFy*
35 34 adantlr φFSMblFnSbyS𝑡DFy*
36 3 2 issmfle φFSMblFnSFSMblFnSDSF:DcyD|FycS𝑡D
37 4 36 mpbid φFSMblFnSDSF:DcyD|FycS𝑡D
38 37 simp3d φFSMblFnScyD|FycS𝑡D
39 10 rabeqdv φFSMblFnSyS𝑡D|Fyc=yD|Fyc
40 39 eleq1d φFSMblFnSyS𝑡D|FycS𝑡DyD|FycS𝑡D
41 40 ralbidv φFSMblFnScyS𝑡D|FycS𝑡DcyD|FycS𝑡D
42 38 41 mpbird φFSMblFnScyS𝑡D|FycS𝑡D
43 42 adantr φFSMblFnSccyS𝑡D|FycS𝑡D
44 simpr φFSMblFnScc
45 rspa cyS𝑡D|FycS𝑡DcyS𝑡D|FycS𝑡D
46 43 44 45 syl2anc φFSMblFnScyS𝑡D|FycS𝑡D
47 46 adantlr φFSMblFnSbcyS𝑡D|FycS𝑡D
48 simpr φFSMblFnSbb
49 18 19 27 28 35 47 48 salpreimalegt φFSMblFnSbyS𝑡D|b<FyS𝑡D
50 13 49 eqeltrd φFSMblFnSbyD|b<FyS𝑡D
51 50 ex φFSMblFnSbyD|b<FyS𝑡D
52 9 51 ralrimi φFSMblFnSbyD|b<FyS𝑡D
53 5 6 52 3jca φFSMblFnSDSF:DbyD|b<FyS𝑡D
54 53 ex φFSMblFnSDSF:DbyD|b<FyS𝑡D
55 nfv yDS
56 nfv yF:D
57 nfcv _y
58 nfrab1 _yyD|b<Fy
59 nfcv _yS𝑡D
60 58 59 nfel yyD|b<FyS𝑡D
61 57 60 nfralw ybyD|b<FyS𝑡D
62 55 56 61 nf3an yDSF:DbyD|b<FyS𝑡D
63 14 62 nfan yφDSF:DbyD|b<FyS𝑡D
64 nfv bDS
65 nfv bF:D
66 nfra1 bbyD|b<FyS𝑡D
67 64 65 66 nf3an bDSF:DbyD|b<FyS𝑡D
68 7 67 nfan bφDSF:DbyD|b<FyS𝑡D
69 1 adantr φDSF:DbyD|b<FyS𝑡DSSAlg
70 simpr1 φDSF:DbyD|b<FyS𝑡DDS
71 simpr2 φDSF:DbyD|b<FyS𝑡DF:D
72 simpr3 φDSF:DbyD|b<FyS𝑡DbyD|b<FyS𝑡D
73 63 68 69 2 70 71 72 issmfgtlem φDSF:DbyD|b<FyS𝑡DFSMblFnS
74 73 ex φDSF:DbyD|b<FyS𝑡DFSMblFnS
75 54 74 impbid φFSMblFnSDSF:DbyD|b<FyS𝑡D
76 breq1 b=ab<Fya<Fy
77 76 rabbidv b=ayD|b<Fy=yD|a<Fy
78 fveq2 y=xFy=Fx
79 78 breq2d y=xa<Fya<Fx
80 79 cbvrabv yD|a<Fy=xD|a<Fx
81 80 a1i b=ayD|a<Fy=xD|a<Fx
82 77 81 eqtrd b=ayD|b<Fy=xD|a<Fx
83 82 eleq1d b=ayD|b<FyS𝑡DxD|a<FxS𝑡D
84 83 cbvralvw byD|b<FyS𝑡DaxD|a<FxS𝑡D
85 84 3anbi3i DSF:DbyD|b<FyS𝑡DDSF:DaxD|a<FxS𝑡D
86 85 a1i φDSF:DbyD|b<FyS𝑡DDSF:DaxD|a<FxS𝑡D
87 75 86 bitrd φFSMblFnSDSF:DaxD|a<FxS𝑡D