Metamath Proof Explorer


Theorem smfpimltxr

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfpimltxr.x _ x F
smfpimltxr.s φ S SAlg
smfpimltxr.f φ F SMblFn S
smfpimltxr.d D = dom F
smfpimltxr.a φ A *
Assertion smfpimltxr φ x D | F x < A S 𝑡 D

Proof

Step Hyp Ref Expression
1 smfpimltxr.x _ x F
2 smfpimltxr.s φ S SAlg
3 smfpimltxr.f φ F SMblFn S
4 smfpimltxr.d D = dom F
5 smfpimltxr.a φ A *
6 breq2 A = +∞ F x < A F x < +∞
7 6 rabbidv A = +∞ x D | F x < A = x D | F x < +∞
8 7 adantl φ A = +∞ x D | F x < A = x D | F x < +∞
9 1 2 4 issmff φ F SMblFn S D S F : D a x D | F x < a S 𝑡 D
10 3 9 mpbid φ D S F : D a x D | F x < a S 𝑡 D
11 10 simp2d φ F : D
12 1 11 pimltpnf2 φ x D | F x < +∞ = D
13 12 adantr φ A = +∞ x D | F x < +∞ = D
14 eqidd φ A = +∞ D = D
15 8 13 14 3eqtrd φ A = +∞ x D | F x < A = D
16 10 simp1d φ D S
17 2 16 restuni4 φ S 𝑡 D = D
18 17 eqcomd φ D = S 𝑡 D
19 3 dmexd φ dom F V
20 4 19 eqeltrid φ D V
21 eqid S 𝑡 D = S 𝑡 D
22 2 20 21 subsalsal φ S 𝑡 D SAlg
23 22 salunid φ S 𝑡 D S 𝑡 D
24 18 23 eqeltrd φ D S 𝑡 D
25 24 adantr φ A = +∞ D S 𝑡 D
26 15 25 eqeltrd φ A = +∞ x D | F x < A S 𝑡 D
27 neqne ¬ A = +∞ A +∞
28 27 adantl φ ¬ A = +∞ A +∞
29 breq2 A = −∞ F x < A F x < −∞
30 29 rabbidv A = −∞ x D | F x < A = x D | F x < −∞
31 30 adantl φ A = −∞ x D | F x < A = x D | F x < −∞
32 11 adantr φ A = −∞ F : D
33 1 32 pimltmnf2 φ A = −∞ x D | F x < −∞ =
34 31 33 eqtrd φ A = −∞ x D | F x < A =
35 22 0sald φ S 𝑡 D
36 35 adantr φ A = −∞ S 𝑡 D
37 34 36 eqeltrd φ A = −∞ x D | F x < A S 𝑡 D
38 37 adantlr φ A +∞ A = −∞ x D | F x < A S 𝑡 D
39 simpll φ A +∞ ¬ A = −∞ φ
40 39 5 syl φ A +∞ ¬ A = −∞ A *
41 neqne ¬ A = −∞ A −∞
42 41 adantl φ A +∞ ¬ A = −∞ A −∞
43 simplr φ A +∞ ¬ A = −∞ A +∞
44 40 42 43 xrred φ A +∞ ¬ A = −∞ A
45 2 adantr φ A S SAlg
46 3 adantr φ A F SMblFn S
47 simpr φ A A
48 1 45 46 4 47 smfpreimaltf φ A x D | F x < A S 𝑡 D
49 39 44 48 syl2anc φ A +∞ ¬ A = −∞ x D | F x < A S 𝑡 D
50 38 49 pm2.61dan φ A +∞ x D | F x < A S 𝑡 D
51 28 50 syldan φ ¬ A = +∞ x D | F x < A S 𝑡 D
52 26 51 pm2.61dan φ x D | F x < A S 𝑡 D