Metamath Proof Explorer


Theorem smfinfmpt

Description: The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfinfmpt.n nφ
smfinfmpt.x xφ
smfinfmpt.y yφ
smfinfmpt.m φM
smfinfmpt.z Z=M
smfinfmpt.s φSSAlg
smfinfmpt.b φnZxABV
smfinfmpt.f φnZxABSMblFnS
smfinfmpt.d D=xnZA|ynZyB
smfinfmpt.g G=xDsuprannZB<
Assertion smfinfmpt φGSMblFnS

Proof

Step Hyp Ref Expression
1 smfinfmpt.n nφ
2 smfinfmpt.x xφ
3 smfinfmpt.y yφ
4 smfinfmpt.m φM
5 smfinfmpt.z Z=M
6 smfinfmpt.s φSSAlg
7 smfinfmpt.b φnZxABV
8 smfinfmpt.f φnZxABSMblFnS
9 smfinfmpt.d D=xnZA|ynZyB
10 smfinfmpt.g G=xDsuprannZB<
11 10 a1i φG=xDsuprannZB<
12 9 a1i φD=xnZA|ynZyB
13 eqidd φnZxAB=nZxAB
14 13 8 fvmpt2d φnZnZxABn=xAB
15 14 dmeqd φnZdomnZxABn=domxAB
16 nfcv _xn
17 nfcv _xZ
18 16 17 nfel xnZ
19 2 18 nfan xφnZ
20 eqid xAB=xAB
21 6 adantr φnZSSAlg
22 7 3expa φnZxABV
23 19 21 22 8 smffmpt φnZxAB:A
24 23 fvmptelrn φnZxAB
25 19 20 24 dmmptdf φnZdomxAB=A
26 eqidd φnZA=A
27 15 25 26 3eqtrrd φnZA=domnZxABn
28 1 27 iineq2d φnZA=nZdomnZxABn
29 nfcv _xnZA
30 nfmpt1 _xxAB
31 17 30 nfmpt _xnZxAB
32 31 16 nffv _xnZxABn
33 32 nfdm _xdomnZxABn
34 17 33 nfiin _xnZdomnZxABn
35 29 34 rabeqf nZA=nZdomnZxABnxnZA|ynZyB=xnZdomnZxABn|ynZyB
36 28 35 syl φxnZA|ynZyB=xnZdomnZxABn|ynZyB
37 nfv yxnZdomnZxABn
38 3 37 nfan yφxnZdomnZxABn
39 nfcv _nx
40 nfii1 _nnZdomnZxABn
41 39 40 nfel nxnZdomnZxABn
42 1 41 nfan nφxnZdomnZxABn
43 simpll φxnZdomnZxABnnZφ
44 simpr φxnZdomnZxABnnZnZ
45 eliinid xnZdomnZxABnnZxdomnZxABn
46 45 adantll φxnZdomnZxABnnZxdomnZxABn
47 27 eqcomd φnZdomnZxABn=A
48 47 adantlr φxnZdomnZxABnnZdomnZxABn=A
49 46 48 eleqtrd φxnZdomnZxABnnZxA
50 14 fveq1d φnZnZxABnx=xABx
51 50 3adant3 φnZxAnZxABnx=xABx
52 simp3 φnZxAxA
53 20 fvmpt2 xABVxABx=B
54 52 7 53 syl2anc φnZxAxABx=B
55 51 54 eqtr2d φnZxAB=nZxABnx
56 55 breq2d φnZxAyBynZxABnx
57 43 44 49 56 syl3anc φxnZdomnZxABnnZyBynZxABnx
58 42 57 ralbida φxnZdomnZxABnnZyBnZynZxABnx
59 38 58 rexbid φxnZdomnZxABnynZyBynZynZxABnx
60 2 59 rabbida φxnZdomnZxABn|ynZyB=xnZdomnZxABn|ynZynZxABnx
61 36 60 eqtrd φxnZA|ynZyB=xnZdomnZxABn|ynZynZxABnx
62 12 61 eqtrd φD=xnZdomnZxABn|ynZynZxABnx
63 2 62 alrimi φxD=xnZdomnZxABn|ynZynZxABnx
64 nfcv _n
65 nfra1 nnZyB
66 64 65 nfrex nynZyB
67 nfii1 _nnZA
68 66 67 nfrabw _nxnZA|ynZyB
69 9 68 nfcxfr _nD
70 39 69 nfel nxD
71 1 70 nfan nφxD
72 simpll φxDnZφ
73 simpr φxDnZnZ
74 9 eleq2i xDxxnZA|ynZyB
75 74 biimpi xDxxnZA|ynZyB
76 rabidim1 xxnZA|ynZyBxnZA
77 75 76 syl xDxnZA
78 77 adantr xDnZxnZA
79 simpr xDnZnZ
80 eliinid xnZAnZxA
81 78 79 80 syl2anc xDnZxA
82 81 adantll φxDnZxA
83 55 idi φnZxAB=nZxABnx
84 72 73 82 83 syl3anc φxDnZB=nZxABnx
85 71 84 mpteq2da φxDnZB=nZnZxABnx
86 85 rneqd φxDrannZB=rannZnZxABnx
87 86 infeq1d φxDsuprannZB<=suprannZnZxABnx<
88 87 ex φxDsuprannZB<=suprannZnZxABnx<
89 2 88 ralrimi φxDsuprannZB<=suprannZnZxABnx<
90 mpteq12f xD=xnZdomnZxABn|ynZynZxABnxxDsuprannZB<=suprannZnZxABnx<xDsuprannZB<=xxnZdomnZxABn|ynZynZxABnxsuprannZnZxABnx<
91 63 89 90 syl2anc φxDsuprannZB<=xxnZdomnZxABn|ynZynZxABnxsuprannZnZxABnx<
92 11 91 eqtrd φG=xxnZdomnZxABn|ynZynZxABnxsuprannZnZxABnx<
93 nfmpt1 _nnZxAB
94 eqid nZxAB=nZxAB
95 1 8 94 fmptdf φnZxAB:ZSMblFnS
96 eqid xnZdomnZxABn|ynZynZxABnx=xnZdomnZxABn|ynZynZxABnx
97 eqid xxnZdomnZxABn|ynZynZxABnxsuprannZnZxABnx<=xxnZdomnZxABn|ynZynZxABnxsuprannZnZxABnx<
98 93 31 4 5 6 95 96 97 smfinf φxxnZdomnZxABn|ynZynZxABnxsuprannZnZxABnx<SMblFnS
99 92 98 eqeltrd φGSMblFnS