Metamath Proof Explorer


Theorem issmfle

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 right-closed intervals unbounded below 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 (ii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 issmfle.s φ S SAlg
2 issmfle.d D = dom F
3 1 adantr φ F SMblFn S S SAlg
4 simpr φ F SMblFn S F SMblFn S
5 3 4 2 smfdmss φ F SMblFn S D S
6 3 4 2 smff φ F SMblFn S F : D
7 nfv b φ
8 nfv b F SMblFn S
9 7 8 nfan b φ F SMblFn S
10 nfv y φ
11 nfv y F SMblFn S
12 10 11 nfan y φ F SMblFn S
13 nfv y b
14 12 13 nfan y φ F SMblFn S b
15 nfv c φ F SMblFn S b
16 1 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 syldan φ F SMblFn S D V
21 eqid S 𝑡 D = S 𝑡 D
22 3 20 21 subsalsal φ F SMblFn S S 𝑡 D SAlg
23 22 adantr φ F SMblFn S b S 𝑡 D SAlg
24 6 frexr φ F SMblFn S F : D *
25 24 adantr φ F SMblFn S b F : D *
26 25 ffvelrnda φ F SMblFn S b y D F y *
27 3 adantr φ F SMblFn S c S SAlg
28 4 adantr φ F SMblFn S c F SMblFn S
29 simpr φ F SMblFn S c c
30 27 28 2 29 smfpreimalt φ F SMblFn S c y D | F y < c S 𝑡 D
31 30 adantlr φ F SMblFn S b c y D | F y < c S 𝑡 D
32 simpr φ F SMblFn S b b
33 14 15 23 26 31 32 salpreimaltle φ F SMblFn S b y D | F y b S 𝑡 D
34 33 ex φ F SMblFn S b y D | F y b S 𝑡 D
35 9 34 ralrimi φ F SMblFn S b y D | F y b S 𝑡 D
36 5 6 35 3jca φ F SMblFn S D S F : D b y D | F y b S 𝑡 D
37 36 ex φ F SMblFn S D S F : D b y D | F y b S 𝑡 D
38 nfv y D S
39 nfv y F : D
40 nfcv _ y
41 nfrab1 _ y y D | F y b
42 nfcv _ y S 𝑡 D
43 41 42 nfel y y D | F y b S 𝑡 D
44 40 43 nfralw y b y D | F y b S 𝑡 D
45 38 39 44 nf3an y D S F : D b y D | F y b S 𝑡 D
46 10 45 nfan y φ D S F : D b y D | F y b S 𝑡 D
47 nfv b D S
48 nfv b F : D
49 nfra1 b b y D | F y b S 𝑡 D
50 47 48 49 nf3an b D S F : D b y D | F y b S 𝑡 D
51 7 50 nfan b φ D S F : D b y D | F y b S 𝑡 D
52 1 adantr φ D S F : D b y D | F y b S 𝑡 D S SAlg
53 simpr1 φ D S F : D b y D | F y b S 𝑡 D D S
54 simpr2 φ D S F : D b y D | F y b S 𝑡 D F : D
55 rspa b y D | F y b S 𝑡 D b y D | F y b S 𝑡 D
56 55 3ad2antl3 D S F : D b y D | F y b S 𝑡 D b y D | F y b S 𝑡 D
57 56 adantll φ D S F : D b y D | F y b S 𝑡 D b y D | F y b S 𝑡 D
58 46 51 52 2 53 54 57 issmflelem φ D S F : D b y D | F y b S 𝑡 D F SMblFn S
59 58 ex φ D S F : D b y D | F y b S 𝑡 D F SMblFn S
60 37 59 impbid φ F SMblFn S D S F : D b y D | F y b S 𝑡 D
61 breq2 b = a F y b F y a
62 61 rabbidv b = a y D | F y b = y D | F y a
63 fveq2 y = x F y = F x
64 63 breq1d y = x F y a F x a
65 64 cbvrabv y D | F y a = x D | F x a
66 65 a1i b = a y D | F y a = x D | F x a
67 62 66 eqtrd b = a y D | F y b = x D | F x a
68 67 eleq1d b = a y D | F y b S 𝑡 D x D | F x a S 𝑡 D
69 68 cbvralvw b y D | F y b S 𝑡 D a x D | F x a S 𝑡 D
70 69 3anbi3i D S F : D b y D | F y b S 𝑡 D D S F : D a x D | F x a S 𝑡 D
71 70 a1i φ D S F : D b y D | F y b S 𝑡 D D S F : D a x D | F x a S 𝑡 D
72 60 71 bitrd φ F SMblFn S D S F : D a x D | F x a S 𝑡 D