Metamath Proof Explorer


Theorem issmflem

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 open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of F is required to be a subset of the underlying set of S . Definition 121C of Fremlin1 p. 36, and Proposition 121B (i) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmflem.s φ S SAlg
issmflem.d D = dom F
Assertion issmflem φ F SMblFn S D S F : D a x D | F x < a S 𝑡 D

Proof

Step Hyp Ref Expression
1 issmflem.s φ S SAlg
2 issmflem.d D = dom F
3 simpr φ F SMblFn S F SMblFn S
4 df-smblfn SMblFn = s SAlg f 𝑝𝑚 s | a f -1 −∞ a s 𝑡 dom f
5 unieq s = S s = S
6 5 oveq2d s = S 𝑝𝑚 s = 𝑝𝑚 S
7 6 rabeqdv s = S f 𝑝𝑚 s | a f -1 −∞ a s 𝑡 dom f = f 𝑝𝑚 S | a f -1 −∞ a s 𝑡 dom f
8 oveq1 s = S s 𝑡 dom f = S 𝑡 dom f
9 8 eleq2d s = S f -1 −∞ a s 𝑡 dom f f -1 −∞ a S 𝑡 dom f
10 9 ralbidv s = S a f -1 −∞ a s 𝑡 dom f a f -1 −∞ a S 𝑡 dom f
11 10 rabbidv s = S f 𝑝𝑚 S | a f -1 −∞ a s 𝑡 dom f = f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f
12 7 11 eqtrd s = S f 𝑝𝑚 s | a f -1 −∞ a s 𝑡 dom f = f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f
13 ovex 𝑝𝑚 S V
14 13 rabex f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f V
15 14 a1i φ f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f V
16 4 12 1 15 fvmptd3 φ SMblFn S = f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f
17 16 adantr φ F SMblFn S SMblFn S = f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f
18 3 17 eleqtrd φ F SMblFn S F f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f
19 elrabi F f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f F 𝑝𝑚 S
20 18 19 syl φ F SMblFn S F 𝑝𝑚 S
21 elpmi2 F 𝑝𝑚 S dom F S
22 2 21 eqsstrid F 𝑝𝑚 S D S
23 22 adantl φ F 𝑝𝑚 S D S
24 20 23 syldan φ F SMblFn S D S
25 elpmi F 𝑝𝑚 S F : dom F dom F S
26 20 25 syl φ F SMblFn S F : dom F dom F S
27 26 simpld φ F SMblFn S F : dom F
28 2 feq2i F : D F : dom F
29 28 a1i φ F SMblFn S F : D F : dom F
30 27 29 mpbird φ F SMblFn S F : D
31 cnveq f = F f -1 = F -1
32 31 imaeq1d f = F f -1 −∞ a = F -1 −∞ a
33 dmeq f = F dom f = dom F
34 33 oveq2d f = F S 𝑡 dom f = S 𝑡 dom F
35 32 34 eleq12d f = F f -1 −∞ a S 𝑡 dom f F -1 −∞ a S 𝑡 dom F
36 35 ralbidv f = F a f -1 −∞ a S 𝑡 dom f a F -1 −∞ a S 𝑡 dom F
37 36 elrab F f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f F 𝑝𝑚 S a F -1 −∞ a S 𝑡 dom F
38 37 simprbi F f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f a F -1 −∞ a S 𝑡 dom F
39 18 38 syl φ F SMblFn S a F -1 −∞ a S 𝑡 dom F
40 39 adantr φ F SMblFn S a a F -1 −∞ a S 𝑡 dom F
41 simpr φ F SMblFn S a a
42 rspa a F -1 −∞ a S 𝑡 dom F a F -1 −∞ a S 𝑡 dom F
43 40 41 42 syl2anc φ F SMblFn S a F -1 −∞ a S 𝑡 dom F
44 30 adantr φ F SMblFn S a F : D
45 simpl F : D a F : D
46 simpr F : D a a
47 46 rexrd F : D a a *
48 45 47 preimaioomnf F : D a F -1 −∞ a = x D | F x < a
49 48 eqcomd F : D a x D | F x < a = F -1 −∞ a
50 44 41 49 syl2anc φ F SMblFn S a x D | F x < a = F -1 −∞ a
51 2 oveq2i S 𝑡 D = S 𝑡 dom F
52 51 a1i φ F SMblFn S a S 𝑡 D = S 𝑡 dom F
53 50 52 eleq12d φ F SMblFn S a x D | F x < a S 𝑡 D F -1 −∞ a S 𝑡 dom F
54 43 53 mpbird φ F SMblFn S a x D | F x < a S 𝑡 D
55 54 ralrimiva φ F SMblFn S a x D | F x < a S 𝑡 D
56 24 30 55 3jca φ F SMblFn S D S F : D a x D | F x < a S 𝑡 D
57 56 ex φ F SMblFn S D S F : D a x D | F x < a S 𝑡 D
58 reex V
59 58 a1i φ D S F : D V
60 1 uniexd φ S V
61 60 adantr φ D S F : D S V
62 simprr φ D S F : D F : D
63 fssxp F : D F D ×
64 63 adantl D S F : D F D ×
65 xpss1 D S D × S ×
66 65 adantr D S F : D D × S ×
67 64 66 sstrd D S F : D F S ×
68 67 adantl φ D S F : D F S ×
69 dmss F S × dom F dom S ×
70 dmxpss dom S × S
71 70 a1i F S × dom S × S
72 69 71 sstrd F S × dom F S
73 72 adantl φ F S × dom F S
74 2 73 eqsstrid φ F S × D S
75 68 74 syldan φ D S F : D D S
76 elpm2r V S V F : D D S F 𝑝𝑚 S
77 59 61 62 75 76 syl22anc φ D S F : D F 𝑝𝑚 S
78 77 3adantr3 φ D S F : D a x D | F x < a S 𝑡 D F 𝑝𝑚 S
79 2 a1i F : D a D = dom F
80 79 oveq2d F : D a S 𝑡 D = S 𝑡 dom F
81 49 80 eleq12d F : D a x D | F x < a S 𝑡 D F -1 −∞ a S 𝑡 dom F
82 81 ralbidva F : D a x D | F x < a S 𝑡 D a F -1 −∞ a S 𝑡 dom F
83 82 biimpd F : D a x D | F x < a S 𝑡 D a F -1 −∞ a S 𝑡 dom F
84 83 imp F : D a x D | F x < a S 𝑡 D a F -1 −∞ a S 𝑡 dom F
85 84 adantl φ F : D a x D | F x < a S 𝑡 D a F -1 −∞ a S 𝑡 dom F
86 85 3adantr1 φ D S F : D a x D | F x < a S 𝑡 D a F -1 −∞ a S 𝑡 dom F
87 78 86 jca φ D S F : D a x D | F x < a S 𝑡 D F 𝑝𝑚 S a F -1 −∞ a S 𝑡 dom F
88 87 37 sylibr φ D S F : D a x D | F x < a S 𝑡 D F f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f
89 16 eqcomd φ f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f = SMblFn S
90 89 adantr φ D S F : D a x D | F x < a S 𝑡 D f 𝑝𝑚 S | a f -1 −∞ a S 𝑡 dom f = SMblFn S
91 88 90 eleqtrd φ D S F : D a x D | F x < a S 𝑡 D F SMblFn S
92 91 ex φ D S F : D a x D | F x < a S 𝑡 D F SMblFn S
93 57 92 impbid φ F SMblFn S D S F : D a x D | F x < a S 𝑡 D