Metamath Proof Explorer


Theorem issmfgtlem

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 a 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 issmfgtlem.x x φ
issmfgtlem.a a φ
issmfgtlem.s φ S SAlg
issmfgtlem.d D = dom F
issmfgtlem.i φ D S
issmfgtlem.f φ F : D
issmfgtlem.p φ a x D | a < F x S 𝑡 D
Assertion issmfgtlem φ F SMblFn S

Proof

Step Hyp Ref Expression
1 issmfgtlem.x x φ
2 issmfgtlem.a a φ
3 issmfgtlem.s φ S SAlg
4 issmfgtlem.d D = dom F
5 issmfgtlem.i φ D S
6 issmfgtlem.f φ F : D
7 issmfgtlem.p φ a x D | a < F x S 𝑡 D
8 3 5 restuni4 φ S 𝑡 D = D
9 8 eqcomd φ D = S 𝑡 D
10 9 rabeqdv φ x D | F x < b = x S 𝑡 D | F x < b
11 10 adantr φ b x D | F x < b = x S 𝑡 D | F x < b
12 nfv x b
13 1 12 nfan x φ b
14 nfv a b
15 2 14 nfan a φ b
16 3 uniexd φ S V
17 16 adantr φ D S S V
18 simpr φ D S D S
19 17 18 ssexd φ D S D V
20 5 19 mpdan φ D V
21 eqid S 𝑡 D = S 𝑡 D
22 3 20 21 subsalsal φ S 𝑡 D SAlg
23 22 adantr φ b S 𝑡 D SAlg
24 eqid S 𝑡 D = S 𝑡 D
25 6 adantr φ x S 𝑡 D F : D
26 simpr φ x S 𝑡 D x S 𝑡 D
27 8 adantr φ x S 𝑡 D S 𝑡 D = D
28 26 27 eleqtrd φ x S 𝑡 D x D
29 25 28 ffvelrnd φ x S 𝑡 D F x
30 29 rexrd φ x S 𝑡 D F x *
31 30 adantlr φ b x S 𝑡 D F x *
32 8 rabeqdv φ x S 𝑡 D | a < F x = x D | a < F x
33 32 adantr φ a x S 𝑡 D | a < F x = x D | a < F x
34 7 r19.21bi φ a x D | a < F x S 𝑡 D
35 33 34 eqeltrd φ a x S 𝑡 D | a < F x S 𝑡 D
36 35 adantlr φ b a x S 𝑡 D | a < F x S 𝑡 D
37 simpr φ b b
38 13 15 23 24 31 36 37 salpreimagtlt φ b x S 𝑡 D | F x < b S 𝑡 D
39 11 38 eqeltrd φ b x D | F x < b S 𝑡 D
40 39 ralrimiva φ b x D | F x < b S 𝑡 D
41 5 6 40 3jca φ D S F : D b x D | F x < b S 𝑡 D
42 3 4 issmf φ F SMblFn S D S F : D b x D | F x < b S 𝑡 D
43 41 42 mpbird φ F SMblFn S