# Metamath Proof Explorer

## Theorem smfpimgtxr

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

Ref Expression
Hypotheses smfpimgtxr.x 𝑥 𝐹
smfpimgtxr.s ( 𝜑𝑆 ∈ SAlg )
smfpimgtxr.f ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
smfpimgtxr.d 𝐷 = dom 𝐹
smfpimgtxr.a ( 𝜑𝐴 ∈ ℝ* )
Assertion smfpimgtxr ( 𝜑 → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )

### Proof

Step Hyp Ref Expression
1 smfpimgtxr.x 𝑥 𝐹
2 smfpimgtxr.s ( 𝜑𝑆 ∈ SAlg )
3 smfpimgtxr.f ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
4 smfpimgtxr.d 𝐷 = dom 𝐹
5 smfpimgtxr.a ( 𝜑𝐴 ∈ ℝ* )
6 breq1 ( 𝐴 = -∞ → ( 𝐴 < ( 𝐹𝑥 ) ↔ -∞ < ( 𝐹𝑥 ) ) )
7 6 rabbidv ( 𝐴 = -∞ → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } = { 𝑥𝐷 ∣ -∞ < ( 𝐹𝑥 ) } )
8 7 adantl ( ( 𝜑𝐴 = -∞ ) → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } = { 𝑥𝐷 ∣ -∞ < ( 𝐹𝑥 ) } )
9 1 nfdm 𝑥 dom 𝐹
10 4 9 nfcxfr 𝑥 𝐷
11 nfcv 𝑦 𝐷
12 nfv 𝑦 -∞ < ( 𝐹𝑥 )
13 nfcv 𝑥 -∞
14 nfcv 𝑥 <
15 nfcv 𝑥 𝑦
16 1 15 nffv 𝑥 ( 𝐹𝑦 )
17 13 14 16 nfbr 𝑥 -∞ < ( 𝐹𝑦 )
18 fveq2 ( 𝑥 = 𝑦 → ( 𝐹𝑥 ) = ( 𝐹𝑦 ) )
19 18 breq2d ( 𝑥 = 𝑦 → ( -∞ < ( 𝐹𝑥 ) ↔ -∞ < ( 𝐹𝑦 ) ) )
20 10 11 12 17 19 cbvrabw { 𝑥𝐷 ∣ -∞ < ( 𝐹𝑥 ) } = { 𝑦𝐷 ∣ -∞ < ( 𝐹𝑦 ) }
21 20 a1i ( 𝜑 → { 𝑥𝐷 ∣ -∞ < ( 𝐹𝑥 ) } = { 𝑦𝐷 ∣ -∞ < ( 𝐹𝑦 ) } )
22 nfv 𝑦 𝜑
23 2 3 4 smff ( 𝜑𝐹 : 𝐷 ⟶ ℝ )
24 23 adantr ( ( 𝜑𝑦𝐷 ) → 𝐹 : 𝐷 ⟶ ℝ )
25 simpr ( ( 𝜑𝑦𝐷 ) → 𝑦𝐷 )
26 24 25 ffvelrnd ( ( 𝜑𝑦𝐷 ) → ( 𝐹𝑦 ) ∈ ℝ )
27 22 26 pimgtmnf ( 𝜑 → { 𝑦𝐷 ∣ -∞ < ( 𝐹𝑦 ) } = 𝐷 )
28 eqidd ( 𝜑𝐷 = 𝐷 )
29 21 27 28 3eqtrd ( 𝜑 → { 𝑥𝐷 ∣ -∞ < ( 𝐹𝑥 ) } = 𝐷 )
30 29 adantr ( ( 𝜑𝐴 = -∞ ) → { 𝑥𝐷 ∣ -∞ < ( 𝐹𝑥 ) } = 𝐷 )
31 8 30 eqtrd ( ( 𝜑𝐴 = -∞ ) → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } = 𝐷 )
32 2 3 4 smfdmss ( 𝜑𝐷 𝑆 )
33 2 32 restuni4 ( 𝜑 ( 𝑆t 𝐷 ) = 𝐷 )
34 33 eqcomd ( 𝜑𝐷 = ( 𝑆t 𝐷 ) )
35 3 dmexd ( 𝜑 → dom 𝐹 ∈ V )
36 4 35 eqeltrid ( 𝜑𝐷 ∈ V )
37 eqid ( 𝑆t 𝐷 ) = ( 𝑆t 𝐷 )
38 2 36 37 subsalsal ( 𝜑 → ( 𝑆t 𝐷 ) ∈ SAlg )
39 38 salunid ( 𝜑 ( 𝑆t 𝐷 ) ∈ ( 𝑆t 𝐷 ) )
40 34 39 eqeltrd ( 𝜑𝐷 ∈ ( 𝑆t 𝐷 ) )
41 40 adantr ( ( 𝜑𝐴 = -∞ ) → 𝐷 ∈ ( 𝑆t 𝐷 ) )
42 31 41 eqeltrd ( ( 𝜑𝐴 = -∞ ) → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
43 neqne ( ¬ 𝐴 = -∞ → 𝐴 ≠ -∞ )
44 43 adantl ( ( 𝜑 ∧ ¬ 𝐴 = -∞ ) → 𝐴 ≠ -∞ )
45 breq1 ( 𝐴 = +∞ → ( 𝐴 < ( 𝐹𝑥 ) ↔ +∞ < ( 𝐹𝑥 ) ) )
46 45 rabbidv ( 𝐴 = +∞ → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } = { 𝑥𝐷 ∣ +∞ < ( 𝐹𝑥 ) } )
47 46 adantl ( ( 𝜑𝐴 = +∞ ) → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } = { 𝑥𝐷 ∣ +∞ < ( 𝐹𝑥 ) } )
48 1 23 pimgtpnf2 ( 𝜑 → { 𝑥𝐷 ∣ +∞ < ( 𝐹𝑥 ) } = ∅ )
49 48 adantr ( ( 𝜑𝐴 = +∞ ) → { 𝑥𝐷 ∣ +∞ < ( 𝐹𝑥 ) } = ∅ )
50 47 49 eqtrd ( ( 𝜑𝐴 = +∞ ) → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } = ∅ )
51 38 0sald ( 𝜑 → ∅ ∈ ( 𝑆t 𝐷 ) )
52 51 adantr ( ( 𝜑𝐴 = +∞ ) → ∅ ∈ ( 𝑆t 𝐷 ) )
53 50 52 eqeltrd ( ( 𝜑𝐴 = +∞ ) → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
54 53 adantlr ( ( ( 𝜑𝐴 ≠ -∞ ) ∧ 𝐴 = +∞ ) → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
55 simpll ( ( ( 𝜑𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝜑 )
56 55 5 syl ( ( ( 𝜑𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝐴 ∈ ℝ* )
57 simplr ( ( ( 𝜑𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝐴 ≠ -∞ )
58 neqne ( ¬ 𝐴 = +∞ → 𝐴 ≠ +∞ )
59 58 adantl ( ( ( 𝜑𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝐴 ≠ +∞ )
60 56 57 59 xrred ( ( ( 𝜑𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝐴 ∈ ℝ )
61 2 adantr ( ( 𝜑𝐴 ∈ ℝ ) → 𝑆 ∈ SAlg )
62 3 adantr ( ( 𝜑𝐴 ∈ ℝ ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
63 simpr ( ( 𝜑𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
64 1 61 62 4 63 smfpreimagtf ( ( 𝜑𝐴 ∈ ℝ ) → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
65 55 60 64 syl2anc ( ( ( 𝜑𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
66 54 65 pm2.61dan ( ( 𝜑𝐴 ≠ -∞ ) → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
67 44 66 syldan ( ( 𝜑 ∧ ¬ 𝐴 = -∞ ) → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
68 42 67 pm2.61dan ( 𝜑 → { 𝑥𝐷𝐴 < ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )